src/HOL/Tools/ATP/atp_problem_generate.ML
changeset 56254 a2dd9200854d
parent 56245 84fc7dfa3cd4
child 56636 bb8b37480d3f
     1.1 --- a/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:16:54 2014 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_problem_generate.ML	Sat Mar 22 18:19:57 2014 +0100
     1.3 @@ -434,7 +434,7 @@
     1.4  fun atp_schematic_consts_of t = add_schematic_consts_of t Symtab.empty
     1.5  
     1.6  val tvar_a_str = "'a"
     1.7 -val tvar_a_z = ((tvar_a_str, 0), HOLogic.typeS)
     1.8 +val tvar_a_z = ((tvar_a_str, 0), @{sort type})
     1.9  val tvar_a = TVar tvar_a_z
    1.10  val tvar_a_name = tvar_name tvar_a_z
    1.11  val itself_name = `make_fixed_type_const @{type_name itself}
    1.12 @@ -2404,7 +2404,7 @@
    1.13  
    1.14  fun rationalize_decls thy (decls as decl :: (decls' as _ :: _)) =
    1.15      let
    1.16 -      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, HOLogic.typeS))
    1.17 +      val T = result_type_of_decl decl |> map_type_tvar (fn (z, _) => TVar (z, @{sort type}))
    1.18      in
    1.19        if forall (type_generalization thy T o result_type_of_decl) decls' then [decl]
    1.20        else decls