src/Pure/goal.ML
changeset 21516 c2a116a2c4fd
parent 20290 3f886c176c9b
child 21579 abd2b4386a63
     1.1 --- a/src/Pure/goal.ML	Fri Nov 24 17:23:15 2006 +0100
     1.2 +++ b/src/Pure/goal.ML	Fri Nov 24 22:05:12 2006 +0100
     1.3 @@ -106,7 +106,7 @@
     1.4  
     1.5  fun prove_multi ctxt xs asms props tac =
     1.6    let
     1.7 -    val thy = Context.theory_of_proof ctxt;
     1.8 +    val thy = ProofContext.theory_of ctxt;
     1.9      val string_of_term = Sign.string_of_term thy;
    1.10  
    1.11      fun err msg = cat_error msg
    1.12 @@ -145,7 +145,7 @@
    1.13  fun prove ctxt xs asms prop tac = hd (prove_multi ctxt xs asms [prop] tac);
    1.14  
    1.15  fun prove_global thy xs asms prop tac =
    1.16 -  Drule.standard (prove (Context.init_proof thy) xs asms prop (fn {prems, ...} => tac prems));
    1.17 +  Drule.standard (prove (ProofContext.init thy) xs asms prop (fn {prems, ...} => tac prems));
    1.18  
    1.19  
    1.20