src/Pure/Isar/calculation.ML
changeset 39557 fe5722fce758
parent 38332 6551e310e7cb
child 42360 da8817d01e7c
--- a/src/Pure/Isar/calculation.ML	Mon Sep 20 15:29:53 2010 +0200
+++ b/src/Pure/Isar/calculation.ML	Mon Sep 20 16:05:25 2010 +0200
@@ -98,7 +98,7 @@
     "declaration of symmetry rule" #>
   Attrib.setup (Binding.name "symmetric") (Scan.succeed symmetric)
     "resolution with symmetry rule" #>
-  PureThy.add_thms
+  Global_Theory.add_thms
    [((Binding.empty, transitive_thm), [trans_add]),
     ((Binding.empty, symmetric_thm), [sym_add])] #> snd));