tuned;
authorwenzelm
Thu Jul 05 00:15:44 2007 +0200 (2007-07-05)
changeset 2358746d01f5e1e5b
parent 23586 7d6b1d800dc4
child 23588 4fc6df2c7098
tuned;
src/Pure/conv.ML
     1.1 --- a/src/Pure/conv.ML	Thu Jul 05 00:06:25 2007 +0200
     1.2 +++ b/src/Pure/conv.ML	Thu Jul 05 00:15:44 2007 +0200
     1.3 @@ -76,11 +76,11 @@
     1.4    let
     1.5      val cache = ref Termtab.empty;
     1.6      fun conv ct =
     1.7 -      (case Termtab.lookup (! cache) (term_of ct) of
     1.8 +      (case Termtab.lookup (! cache) (Thm.term_of ct) of
     1.9          SOME th => th
    1.10        | NONE =>
    1.11            let val th = cv ct
    1.12 -          in change cache (Termtab.update (term_of ct, th)); th end);
    1.13 +          in change cache (Termtab.update (Thm.term_of ct, th)); th end);
    1.14   in conv end;
    1.15  
    1.16  
    1.17 @@ -90,7 +90,7 @@
    1.18  (* lambda terms *)
    1.19  
    1.20  fun abs_conv cv ct =
    1.21 -  (case term_of ct of
    1.22 +  (case Thm.term_of ct of
    1.23      Abs (x, _, _) =>
    1.24        let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct
    1.25        in Thm.abstract_rule x v (cv ct') end
    1.26 @@ -118,7 +118,7 @@
    1.27        (case try Thm.dest_comb ct of
    1.28          NONE => cv ct
    1.29        | SOME (A, B) =>
    1.30 -          (case (term_of A, term_of B) of
    1.31 +          (case (Thm.term_of A, Thm.term_of B) of
    1.32              (Const ("all", _), Abs (x, _, _)) =>
    1.33                let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in
    1.34                  Thm.combination (all_conv A)