src/Pure/subgoal.ML
changeset 42360 da8817d01e7c
parent 34075 451b0c8a15cf
child 42495 1af81b70cf09
     1.1 --- a/src/Pure/subgoal.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/subgoal.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -67,7 +67,7 @@
     1.4  *)
     1.5  fun lift_import idx params th ctxt =
     1.6    let
     1.7 -    val cert = Thm.cterm_of (ProofContext.theory_of ctxt);
     1.8 +    val cert = Thm.cterm_of (Proof_Context.theory_of ctxt);
     1.9      val ((_, [th']), ctxt') = Variable.importT [th] ctxt;
    1.10  
    1.11      val Ts = map (#T o Thm.rep_cterm) params;