1.1 --- a/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Sep 20 15:29:53 2010 +0200
     1.2 +++ b/src/HOL/Tools/SMT/z3_proof_reconstruction.ML	Mon Sep 20 16:05:25 2010 +0200
     1.3 @@ -57,7 +57,7 @@
     1.4  
     1.5  val z3_rules_setup =
     1.6    Attrib.setup (Binding.name z3_ruleN) (Attrib.add_del add del) description #>
     1.7 -  PureThy.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
     1.8 +  Global_Theory.add_thms_dynamic (Binding.name z3_ruleN, Net.content o Z3_Rules.get)
     1.9  
    1.10  end
    1.11