src/HOL/Tools/Predicate_Compile/code_prolog.ML

     Const ("==>", _) $ _ $ _ => Conv.combination_conv (Conv.arg_conv cv) (imp_prems_conv cv) ct
   | _ => Conv.all_conv ct
 
 fun Trueprop_conv cv ct =
   case Thm.term_of ct of
-    Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct  
+    Const (@{const_name Trueprop}, _) $ _ => Conv.arg_conv cv ct  
   | _ => raise Fail "Trueprop_conv"
 
 fun preprocess_intro thy rule =
   Conv.fconv_rule
     (imp_prems_conv