src/HOL/Tools/datatype_package.ML
changeset 26939 1035c89b4c02
parent 26533 aeef55a3d1d5
child 27002 215d64dc971e
     1.1 --- a/src/HOL/Tools/datatype_package.ML	Sat May 17 23:53:20 2008 +0200
     1.2 +++ b/src/HOL/Tools/datatype_package.ML	Sun May 18 15:04:09 2008 +0200
     1.3 @@ -563,7 +563,7 @@
     1.4        Variable.importT_thms [induction] (Variable.thm_context induction);
     1.5  
     1.6      fun err t = error ("Ill-formed predicate in induction rule: " ^
     1.7 -      Sign.string_of_term thy1 t);
     1.8 +      Syntax.string_of_term_global thy1 t);
     1.9  
    1.10      fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
    1.11            ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)