src/HOL/Tools/Meson/meson.ML
changeset 60642 48dd1cefb4ae
parent 60362 befdc10ebb42
child 60696 8304fb4fb823
     1.1 --- a/src/HOL/Tools/Meson/meson.ML	Fri Jul 03 16:19:45 2015 +0200
     1.2 +++ b/src/HOL/Tools/Meson/meson.ML	Sun Jul 05 15:02:30 2015 +0200
     1.3 @@ -346,16 +346,17 @@
     1.4  (*Replaces universally quantified variables by FREE variables -- because
     1.5    assumptions may not contain scheme variables.  Later, generalize using Variable.export. *)
     1.6  local  
     1.7 -  val spec_var = Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))));
     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 +  val spec_var =
    1.11 +    Thm.dest_arg (Thm.dest_arg (#2 (Thm.dest_implies (Thm.cprop_of spec))))
    1.12 +    |> Thm.term_of |> dest_Var;
    1.13 +  fun name_of (Const (@{const_name All}, _) $ Abs(x, _, _)) = x | name_of _ = Name.uu;
    1.14  in  
    1.15    fun freeze_spec th ctxt =
    1.16      let
    1.17        val ([x], ctxt') =
    1.18          Variable.variant_fixes [name_of (HOLogic.dest_Trueprop (Thm.concl_of th))] ctxt;
    1.19        val spec' = spec
    1.20 -        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, spec_varT)))]);
    1.21 +        |> Thm.instantiate ([], [(spec_var, Thm.cterm_of ctxt' (Free (x, snd spec_var)))]);
    1.22      in (th RS spec', ctxt') end
    1.23  end;
    1.24