# HG changeset patch
# User haftmann
# Date 1196860572 -3600
# Node ID e209975d56061d29d77a0284a2bd73763f6561f7
# Parent  8b7ed8aef0011418c0739c657297150cf1c9bf62
added constrain_thm

diff -r 8b7ed8aef001 -r e209975d5606 src/Pure/Isar/code_unit.ML
--- 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;