src/Tools/Code/code_thingol.ML
changeset 35845 e5980f0ad025
parent 35299 4f4d5bf4ea08
child 35961 00e48e1d9afd
     1.1 --- a/src/Tools/Code/code_thingol.ML	Sat Mar 20 02:23:41 2010 +0100
     1.2 +++ b/src/Tools/Code/code_thingol.ML	Sat Mar 20 17:33:11 2010 +0100
     1.3 @@ -613,7 +613,7 @@
     1.4        let
     1.5          val c_inst = Const (c, map_type_tfree (K arity_typ') ty);
     1.6          val thm = AxClass.unoverload_conv thy (Thm.cterm_of thy c_inst);
     1.7 -        val c_ty = (apsnd Logic.unvarifyT o dest_Const o snd
     1.8 +        val c_ty = (apsnd Logic.unvarifyT_global o dest_Const o snd
     1.9            o Logic.dest_equals o Thm.prop_of) thm;
    1.10        in
    1.11          ensure_const thy algbr eqngr c