src/HOL/Tools/Sledgehammer/metis_tactics.ML
changeset 36967 3c804030474b
parent 36966 adc11fb3f3aa
child 37318 32b3d16b04f6
equal deleted inserted replaced
36966:adc11fb3f3aa 36967:3c804030474b
   214   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   214   in  TFree(ww, the_default HOLogic.typeS (Variable.def_sort ctxt (ww, ~1)))  end;
   215 
   215 
   216 (*Remove the "apply" operator from an HO term*)
   216 (*Remove the "apply" operator from an HO term*)
   217 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   217 fun strip_happ args (Metis.Term.Fn(".",[t,u])) = strip_happ (u::args) t
   218   | strip_happ args x = (x, args);
   218   | strip_happ args x = (x, args);
       
   219 
       
   220 fun make_tvar s = TVar (("'" ^ s, 0), HOLogic.typeS)
   219 
   221 
   220 fun fol_type_to_isa _ (Metis.Term.Var v) =
   222 fun fol_type_to_isa _ (Metis.Term.Var v) =
   221      (case strip_prefix tvar_prefix v of
   223      (case strip_prefix tvar_prefix v of
   222           SOME w => make_tvar w
   224           SOME w => make_tvar w
   223         | NONE   => make_tvar v)
   225         | NONE   => make_tvar v)