# HG changeset patch
# User haftmann
# Date 1242232900 -7200
# Node ID a51ce445d4989b94dcff07b9aa70f33666c15aed
# Parent  cd3aafc1c631d690b83cc7e2b3daf5fa99f8c3cc
dropped legacy operations

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;
diff -r cd3aafc1c631 -r a51ce445d498 src/Tools/quickcheck.ML
--- a/src/Tools/quickcheck.ML	Wed May 13 18:41:39 2009 +0200
+++ b/src/Tools/quickcheck.ML	Wed May 13 18:41:40 2009 +0200
@@ -94,7 +94,7 @@
       error "Term to be tested contains type variables";
     val _ = null (Term.add_vars t []) orelse
       error "Term to be tested contains schematic variables";
-    val frees = map dest_Free (OldTerm.term_frees t);
+    val frees = Term.add_frees t [];
   in (map fst frees, list_abs_free (frees, t)) end
 
 fun test_term ctxt quiet generator_name size i t =