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
```