--- a/src/Pure/Isar/code_unit.ML Wed Dec 05 14:16:11 2007 +0100
+++ b/src/Pure/Isar/code_unit.ML Wed Dec 05 14:16:12 2007 +0100
@@ -17,6 +17,7 @@
val typ_sort_inst: Sorts.algebra -> typ * sort
-> sort Vartab.table -> sort Vartab.table
val inst_thm: sort Vartab.table -> thm -> thm
+ val constrain_thm: sort -> thm -> thm
(*constants*)
val string_of_typ: theory -> typ -> string
@@ -253,6 +254,16 @@
val insts = map_filter mk_inst tvars;
in Thm.instantiate (insts, []) thm end;
+fun constrain_thm sort thm =
+ let
+ val thy = Thm.theory_of_thm thm;
+ val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
+ val tvars = (Term.add_tvars o Thm.prop_of) thm [];
+ fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
+ (sort, constrain sort)
+ val insts = map mk_inst tvars;
+ in Thm.instantiate (insts, []) thm end;
+
fun expand_eta k thm =
let
val thy = Thm.theory_of_thm thm;