| 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));