dropped legacy operations
authorhaftmann
Wed May 13 18:41:40 2009 +0200 (2009-05-13)
changeset 31138a51ce445d498
parent 31137 cd3aafc1c631
child 31139 0b615ac7eeaf
dropped legacy operations
src/Pure/Isar/code_unit.ML
src/Tools/quickcheck.ML
     1.1 --- a/src/Pure/Isar/code_unit.ML	Wed May 13 18:41:39 2009 +0200
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Wed May 13 18:41:40 2009 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4    (*typ instantiations*)
     1.5    val typscheme: theory -> string * typ -> (string * sort) list * typ
     1.6    val inst_thm: theory -> sort Vartab.table -> thm -> thm
     1.7 -  val constrain_thm: theory -> sort -> thm -> thm
     1.8  
     1.9    (*constant aliasses*)
    1.10    val add_const_alias: thm -> theory -> theory
    1.11 @@ -80,15 +79,6 @@
    1.12      val insts = map_filter mk_inst tvars;
    1.13    in Thm.instantiate (insts, []) thm end;
    1.14  
    1.15 -fun constrain_thm thy sort thm =
    1.16 -  let
    1.17 -    val constrain = curry (Sorts.inter_sort (Sign.classes_of thy)) sort
    1.18 -    val tvars = (Term.add_tvars o Thm.prop_of) thm [];
    1.19 -    fun mk_inst (tvar as (v, sort)) = pairself (Thm.ctyp_of thy o TVar o pair v)
    1.20 -      (sort, constrain sort)
    1.21 -    val insts = map mk_inst tvars;
    1.22 -  in Thm.instantiate (insts, []) thm end;
    1.23 -
    1.24  fun expand_eta thy k thm =
    1.25    let
    1.26      val (lhs, rhs) = (Logic.dest_equals o Thm.plain_prop_of) thm;
     2.1 --- a/src/Tools/quickcheck.ML	Wed May 13 18:41:39 2009 +0200
     2.2 +++ b/src/Tools/quickcheck.ML	Wed May 13 18:41:40 2009 +0200
     2.3 @@ -94,7 +94,7 @@
     2.4        error "Term to be tested contains type variables";
     2.5      val _ = null (Term.add_vars t []) orelse
     2.6        error "Term to be tested contains schematic variables";
     2.7 -    val frees = map dest_Free (OldTerm.term_frees t);
     2.8 +    val frees = Term.add_frees t [];
     2.9    in (map fst frees, list_abs_free (frees, t)) end
    2.10  
    2.11  fun test_term ctxt quiet generator_name size i t =