# HG changeset patch # User wenzelm # Date 1183587344 -7200 # Node ID 46d01f5e1e5b5480a495b3ef3ceb499b53e6b037 # Parent 7d6b1d800dc42b52d8c1e49451108217ed85ae1e tuned; diff -r 7d6b1d800dc4 -r 46d01f5e1e5b src/Pure/conv.ML --- a/src/Pure/conv.ML Thu Jul 05 00:06:25 2007 +0200 +++ b/src/Pure/conv.ML Thu Jul 05 00:15:44 2007 +0200 @@ -76,11 +76,11 @@ let val cache = ref Termtab.empty; fun conv ct = - (case Termtab.lookup (! cache) (term_of ct) of + (case Termtab.lookup (! cache) (Thm.term_of ct) of SOME th => th | NONE => let val th = cv ct - in change cache (Termtab.update (term_of ct, th)); th end); + in change cache (Termtab.update (Thm.term_of ct, th)); th end); in conv end; @@ -90,7 +90,7 @@ (* lambda terms *) fun abs_conv cv ct = - (case term_of ct of + (case Thm.term_of ct of Abs (x, _, _) => let val (v, ct') = Thm.dest_abs (SOME (gensym "abs_")) ct in Thm.abstract_rule x v (cv ct') end @@ -118,7 +118,7 @@ (case try Thm.dest_comb ct of NONE => cv ct | SOME (A, B) => - (case (term_of A, term_of B) of + (case (Thm.term_of A, Thm.term_of B) of (Const ("all", _), Abs (x, _, _)) => let val (v, B') = Thm.dest_abs (SOME (gensym "all_")) B in Thm.combination (all_conv A)