src/ZF/Tools/inductive_package.ML

--- a/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:19:27 2010 +0200
+++ b/src/ZF/Tools/inductive_package.ML	Wed Aug 18 12:26:48 2010 +0200
@@ -102,7 +102,7 @@
 
   val z' = mk_variant"z" and X' = mk_variant"X" and w' = mk_variant"w";
 
-  fun dest_tprop (Const("Trueprop",_) $ P) = P
+  fun dest_tprop (Const(@{const_name Trueprop},_) $ P) = P
     | dest_tprop Q = error ("Ill-formed premise of introduction rule: " ^
                             Syntax.string_of_term ctxt Q);