src/Pure/Proof/extraction.ML
changeset 32738 15bb09ca0378
parent 32035 8e77b6a250d5
child 32784 1a5dde5079ac
     1.1 --- a/src/Pure/Proof/extraction.ML	Tue Sep 29 11:48:32 2009 +0200
     1.2 +++ b/src/Pure/Proof/extraction.ML	Tue Sep 29 11:49:22 2009 +0200
     1.3 @@ -91,7 +91,7 @@
     1.4        Pattern.rewrite_term thy [] (condrew' :: procs) tm
     1.5      and condrew' tm =
     1.6        let
     1.7 -        val cache = ref ([] : (term * term) list);
     1.8 +        val cache = Unsynchronized.ref ([] : (term * term) list);
     1.9          fun lookup f x = (case AList.lookup (op =) (!cache) x of
    1.10              NONE =>
    1.11                let val y = f x