src/Pure/Isar/skip_proof.ML
changeset 42360 da8817d01e7c
parent 36610 bafd82950e24
child 42409 3e1e80df6a42
     1.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -35,10 +35,10 @@
     1.4    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     1.5      (fn args => fn st =>
     1.6        if ! quick_and_dirty
     1.7 -      then cheat_tac (ProofContext.theory_of ctxt) st
     1.8 +      then cheat_tac (Proof_Context.theory_of ctxt) st
     1.9        else tac args st);
    1.10  
    1.11  fun prove_global thy xs asms prop tac =
    1.12 -  Drule.export_without_context (prove (ProofContext.init_global thy) xs asms prop tac);
    1.13 +  Drule.export_without_context (prove (Proof_Context.init_global thy) xs asms prop tac);
    1.14  
    1.15  end;