diff -r cd3aafc1c631 -r a51ce445d498 src/Pure/Isar/code_unit.ML
--- 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;