1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Apr 16 15:47:52 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Sat Apr 16 16:15:37 2011 +0200
     1.3 @@ -95,7 +95,7 @@
     1.4    | mk_type thy ty =
     1.5        (case get_type thy ty of
     1.6           NONE =>
     1.7 -           Syntax.check_typ (ProofContext.init_global thy)
     1.8 +           Syntax.check_typ (Proof_Context.init_global thy)
     1.9               (Type (Sign.full_name thy (Binding.name ty), []))
    1.10         | SOME T => T);
    1.11  
    1.12 @@ -108,8 +108,8 @@
    1.13        Logic.dest_equals |>> dest_Free;
    1.14      val ((_, (_, thm)), lthy') = Local_Theory.define
    1.15        ((Binding.name c, NoSyn), ((Binding.name def_name, []), rhs)) lthy
    1.16 -    val ctxt_thy = ProofContext.init_global (ProofContext.theory_of lthy');
    1.17 -    val thm' = singleton (ProofContext.export lthy' ctxt_thy) thm
    1.18 +    val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy');
    1.19 +    val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm
    1.20    in (thm', lthy') end;
    1.21  
    1.22  fun strip_underscores s =
    1.23 @@ -183,7 +183,7 @@
    1.24           rtac @{thm subset_antisym} 1 THEN
    1.25           rtac @{thm subsetI} 1 THEN
    1.26           Datatype_Aux.exh_tac (K (#exhaust (Datatype_Data.the_info
    1.27 -           (ProofContext.theory_of lthy) tyname'))) 1 THEN
    1.28 +           (Proof_Context.theory_of lthy) tyname'))) 1 THEN
    1.29           ALLGOALS (asm_full_simp_tac (simpset_of lthy)));
    1.30  
    1.31      val finite_UNIV = Goal.prove lthy [] []
    1.32 @@ -904,7 +904,7 @@
    1.33           val ((t', (_, th)), lthy') = Specification.definition
    1.34             (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.35               (Free (s, T), t)))) lthy;
    1.36 -         val phi = ProofContext.export_morphism lthy' lthy
    1.37 +         val phi = Proof_Context.export_morphism lthy' lthy
    1.38         in
    1.39           ((id', Morphism.thm phi th),
    1.40            ((Symtab.update (s, (Morphism.term phi t', ty)) tab,