theory Scratch imports Main begin
  
ML {*
val tm = Syntax.read_term @{context} 
  "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))" ;
val ty = Term.type_of tm ;
*}


lemma test: "Pure.imp (HOL.Trueprop (A)) (HOL.Trueprop (A))"
(* error message is 
Type unification failed: Clash of types "prop" and "bool"

Type error in application: incompatible operand type

Operator:  Trueprop :: bool \<Rightarrow> prop
Operand:   A \<Longrightarrow> A :: prop
*)