--- a/src/Pure/Isar/code_unit.ML Wed May 13 18:41:39 2009 +0200
+++ b/src/Pure/Isar/code_unit.ML Wed May 13 18:41:40 2009 +0200
@@ -9,7 +9,6 @@
(*typ instantiations*)
val typscheme: theory -> string * typ -> (string * sort) list * typ
val inst_thm: theory -> sort Vartab.table -> thm -> thm
- val constrain_thm: theory -> sort -> thm -> thm
(*constant aliasses*)
val add_const_alias: thm -> theory -> theory
@@ -80,15 +79,6 @@
val insts = map_filter mk_inst tvars;
in Thm.instantiate (insts, []) thm end;
-fun constrain_thm thy sort thm =
- let
- 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 thy k thm =
let
val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;