src/HOL/Import/import.ML
changeset 42361 23f352990944
parent 36945 9bec62c10714
child 46799 f21494dc0bf6
     1.1 --- a/src/HOL/Import/import.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/Import/import.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -25,11 +25,11 @@
     1.4  
     1.5  fun import_tac ctxt (thyname, thmname) =
     1.6      if ! quick_and_dirty
     1.7 -    then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
     1.8 +    then Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)
     1.9      else
    1.10       fn th =>
    1.11          let
    1.12 -            val thy = ProofContext.theory_of ctxt
    1.13 +            val thy = Proof_Context.theory_of ctxt
    1.14              val prem = hd (prems_of th)
    1.15              val _ = message ("Import_tac: thyname=" ^ thyname ^ ", thmname=" ^ thmname)
    1.16              val _ = message ("Import trying to prove " ^ Syntax.string_of_term ctxt prem)