src/Pure/Isar/element.ML
changeset 52230 1105b3b5aa77
parent 49750 444cfaa331c9
child 52732 b4da1f2ec73f
--- a/src/Pure/Isar/element.ML	Thu May 30 08:27:51 2013 +0200
+++ b/src/Pure/Isar/element.ML	Thu May 30 12:35:40 2013 +0200
@@ -466,7 +466,7 @@
        {binding = [],
         typ = [],
         term = [Raw_Simplifier.rewrite_term thy thms []],
-        fact = [map (Raw_Simplifier.rewrite_rule thms)]});
+        fact = [map (rewrite_rule thms)]});
 
 
 (* transfer to theory using closure *)