src/Pure/Isar/class_target.ML
changeset 36610 bafd82950e24
parent 36462 70a1e6accac3
child 36672 bd7f659f7de5
     1.1 --- a/src/Pure/Isar/class_target.ML	Mon May 03 07:59:51 2010 +0200
     1.2 +++ b/src/Pure/Isar/class_target.ML	Mon May 03 14:25:56 2010 +0200
     1.3 @@ -157,7 +157,7 @@
     1.4  
     1.5  fun print_classes thy =
     1.6    let
     1.7 -    val ctxt = ProofContext.init thy;
     1.8 +    val ctxt = ProofContext.init_global thy;
     1.9      val algebra = Sign.classes_of thy;
    1.10      val arities =
    1.11        Symtab.empty
    1.12 @@ -372,7 +372,7 @@
    1.13        ProofContext.theory ((fold o fold) AxClass.add_classrel results);
    1.14    in
    1.15      thy
    1.16 -    |> ProofContext.init
    1.17 +    |> ProofContext.init_global
    1.18      |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
    1.19    end;
    1.20  
    1.21 @@ -421,7 +421,7 @@
    1.22  
    1.23  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    1.24    let
    1.25 -    val ctxt = ProofContext.init thy;
    1.26 +    val ctxt = ProofContext.init_global thy;
    1.27      val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
    1.28        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    1.29      val tycos = map #1 all_arities;
    1.30 @@ -514,7 +514,7 @@
    1.31    in
    1.32      thy
    1.33      |> Theory.checkpoint
    1.34 -    |> ProofContext.init
    1.35 +    |> ProofContext.init_global
    1.36      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
    1.37      |> fold (Variable.declare_typ o TFree) vs
    1.38      |> fold (Variable.declare_names o Free o snd) params
    1.39 @@ -554,7 +554,7 @@
    1.40  fun prove_instantiation_exit_result f tac x lthy =
    1.41    let
    1.42      val morph = ProofContext.export_morphism lthy
    1.43 -      (ProofContext.init (ProofContext.theory_of lthy));
    1.44 +      (ProofContext.init_global (ProofContext.theory_of lthy));
    1.45      val y = f morph x;
    1.46    in
    1.47      lthy
    1.48 @@ -597,7 +597,7 @@
    1.49        ((fold o fold) AxClass.add_arity results);
    1.50    in
    1.51      thy
    1.52 -    |> ProofContext.init
    1.53 +    |> ProofContext.init_global
    1.54      |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
    1.55    end;
    1.56