src/HOL/Tools/Meson/meson.ML
changeset 59586 ddf6deaadfe8
parent 59582 0fbed69ff081
child 59617 b60e65ad13df
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Wed Mar 04 20:50:20 2015 +0100
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Wed Mar 04 22:05:01 2015 +0100
     1.3 @@ -347,7 +347,7 @@
     1.4    assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
     1.5  local  
     1.6    val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
     1.7 -  val spec_varT = #T (Thm.rep_cterm spec_var);
     1.8 +  val spec_varT = Thm.typ_of_cterm spec_var;
     1.9    fun name_of (Const (@{const_name All}, _) $ Abs(x,_,_)) = x | name_of _ = Name.uu;
    1.10  in  
    1.11    fun freeze_spec th ctxt =