src/Pure/Proof/extraction.ML
changeset 17203 29b2563f5c11
parent 17057 0934ac31985f
child 17223 430edc6b7826
     1.1 --- a/src/Pure/Proof/extraction.ML	Wed Aug 31 15:46:39 2005 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Wed Aug 31 15:46:40 2005 +0200
     1.3 @@ -88,10 +88,8 @@
     1.4  
     1.5  fun condrew thy rules procs =
     1.6    let
     1.7 -    val tsig = Sign.tsig_of thy;
     1.8 -
     1.9      fun rew tm =
    1.10 -      Pattern.rewrite_term tsig [] (condrew' :: procs) tm
    1.11 +      Pattern.rewrite_term thy [] (condrew' :: procs) tm
    1.12      and condrew' tm =
    1.13        let
    1.14          val cache = ref ([] : (term * term) list);
    1.15 @@ -105,7 +103,7 @@
    1.16          let
    1.17            fun ren t = getOpt (Term.rename_abs tm1 tm t, t);
    1.18            val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1);
    1.19 -          val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm);
    1.20 +          val env as (Tenv, tenv) = Pattern.match thy (inc tm1, tm);
    1.21            val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems;
    1.22            val env' = Envir.Envir
    1.23              {maxidx = Library.foldl Int.max
    1.24 @@ -321,7 +319,7 @@
    1.25      let
    1.26        val name = Thm.name_of_thm thm;
    1.27        val _ = assert (name <> "") "add_realizers: unnamed theorem";
    1.28 -      val prop = Pattern.rewrite_term (Sign.tsig_of thy')
    1.29 +      val prop = Pattern.rewrite_term thy'
    1.30          (map (Logic.dest_equals o prop_of) defs) [] (prop_of thm);
    1.31        val vars = vars_of prop;
    1.32        val vars' = filter_out (fn v =>
    1.33 @@ -350,7 +348,7 @@
    1.34        ExtractionData.get thy';
    1.35      val procs = List.concat (map (fst o snd) types);
    1.36      val eqns = Net.merge (K false) (#net realizes_eqns, #net typeof_eqns);
    1.37 -    val prop' = Pattern.rewrite_term (Sign.tsig_of thy')
    1.38 +    val prop' = Pattern.rewrite_term thy'
    1.39        (map (Logic.dest_equals o prop_of) defs) [] prop;
    1.40    in freeze_thaw (condrew thy' eqns
    1.41      (procs @ [typeof_proc (Sign.defaultS thy') vs, rlz_proc]))