changeset 38549 | d0385f2764d8 |
parent 38504 | 76965c356d2a |
child 38558 | 32ad17fe2b9c |
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 10:27:12 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Thu Aug 19 11:02:14 2010 +0200 @@ -147,7 +147,7 @@ fun Trueprop_conv cv ct = case Thm.term_of ct of - Const ("Trueprop", _) $ _ => Conv.arg_conv cv ct + Const (@{const_name "Trueprop"}, _) $ _ => Conv.arg_conv cv ct | _ => raise Fail "Trueprop_conv" fun preprocess_intro thy rule =