src/Pure/Isar/class.ML
changeset 42360 da8817d01e7c
parent 42359 6ca5407863ed
child 42375 774df7c59508
     1.1 --- a/src/Pure/Isar/class.ML	Sat Apr 16 15:25:25 2011 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Apr 16 15:47:52 2011 +0200
     1.3 @@ -151,7 +151,7 @@
     1.4  
     1.5  fun print_classes ctxt =
     1.6    let
     1.7 -    val thy = ProofContext.theory_of ctxt;
     1.8 +    val thy = Proof_Context.theory_of ctxt;
     1.9      val algebra = Sign.classes_of thy;
    1.10      val arities =
    1.11        Symtab.empty
    1.12 @@ -164,10 +164,10 @@
    1.13          val Ss = Sorts.mg_domain algebra tyco [class];
    1.14        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    1.15      fun mk_param (c, ty) =
    1.16 -      Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^
    1.17 +      Pretty.str (Proof_Context.extern_const ctxt c ^ " :: " ^
    1.18          Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
    1.19      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.20 -      (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"),
    1.21 +      (SOME o Pretty.str) ("class " ^ Proof_Context.extern_class ctxt class ^ ":"),
    1.22        (SOME o Pretty.block) [Pretty.str "supersort: ",
    1.23          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.24        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
    1.25 @@ -257,7 +257,7 @@
    1.26  
    1.27  fun synchronize_class_syntax sort base_sort ctxt =
    1.28    let
    1.29 -    val thy = ProofContext.theory_of ctxt;
    1.30 +    val thy = Proof_Context.theory_of ctxt;
    1.31      val algebra = Sign.classes_of thy;
    1.32      val operations = these_operations thy sort;
    1.33      fun subst_class_typ sort = map_type_tfree (K (TVar ((Name.aT, 0), sort)));
    1.34 @@ -310,7 +310,7 @@
    1.35    lthy
    1.36    |> Local_Theory.raw_theory f
    1.37    |> Local_Theory.target (synchronize_class_syntax [class]
    1.38 -      (base_sort (ProofContext.theory_of lthy) class));
    1.39 +      (base_sort (Proof_Context.theory_of lthy) class));
    1.40  
    1.41  local
    1.42  
    1.43 @@ -369,10 +369,10 @@
    1.44  fun gen_classrel mk_prop classrel thy =
    1.45    let
    1.46      fun after_qed results =
    1.47 -      ProofContext.background_theory ((fold o fold) AxClass.add_classrel results);
    1.48 +      Proof_Context.background_theory ((fold o fold) AxClass.add_classrel results);
    1.49    in
    1.50      thy
    1.51 -    |> ProofContext.init_global
    1.52 +    |> Proof_Context.init_global
    1.53      |> Proof.theorem NONE after_qed [[(mk_prop thy classrel, [])]]
    1.54    end;
    1.55  
    1.56 @@ -421,8 +421,8 @@
    1.57  
    1.58  fun read_multi_arity thy (raw_tycos, raw_sorts, raw_sort) =
    1.59    let
    1.60 -    val ctxt = ProofContext.init_global thy;
    1.61 -    val all_arities = map (fn raw_tyco => ProofContext.read_arity ctxt
    1.62 +    val ctxt = Proof_Context.init_global thy;
    1.63 +    val all_arities = map (fn raw_tyco => Proof_Context.read_arity ctxt
    1.64        (raw_tyco, raw_sorts, raw_sort)) raw_tycos;
    1.65      val tycos = map #1 all_arities;
    1.66      val (_, sorts, sort) = hd all_arities;
    1.67 @@ -437,7 +437,7 @@
    1.68      val Instantiation { params, ... } = Instantiation.get ctxt;
    1.69  
    1.70      val lookup_inst_param = AxClass.lookup_inst_param
    1.71 -      (Sign.consts_of (ProofContext.theory_of ctxt)) params;
    1.72 +      (Sign.consts_of (Proof_Context.theory_of ctxt)) params;
    1.73      fun subst (c, ty) = case lookup_inst_param (c, ty)
    1.74       of SOME (v_ty as (_, ty)) => SOME (ty, Free v_ty)
    1.75        | NONE => NONE;
    1.76 @@ -498,23 +498,23 @@
    1.77  fun pretty lthy =
    1.78    let
    1.79      val { arities = (tycos, vs, sort), params } = the_instantiation lthy;
    1.80 -    val thy = ProofContext.theory_of lthy;
    1.81 +    val thy = Proof_Context.theory_of lthy;
    1.82      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    1.83      fun pr_param ((c, _), (v, ty)) =
    1.84        Pretty.block (Pretty.breaks
    1.85 -        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
    1.86 +        [Pretty.str v, Pretty.str "==", Pretty.str (Proof_Context.extern_const lthy c),
    1.87            Pretty.str "::", Syntax.pretty_typ lthy ty]);
    1.88    in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
    1.89  
    1.90  fun conclude lthy =
    1.91    let
    1.92      val (tycos, vs, sort) = #arities (the_instantiation lthy);
    1.93 -    val thy = ProofContext.theory_of lthy;
    1.94 +    val thy = Proof_Context.theory_of lthy;
    1.95      val _ = tycos |> List.app (fn tyco =>
    1.96        if Sign.of_sort thy
    1.97          (Type (tyco, map TFree vs), sort)
    1.98        then ()
    1.99 -      else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco)));
   1.100 +      else error ("Missing instance proof for type " ^ quote (Proof_Context.extern_type lthy tyco)));
   1.101    in lthy end;
   1.102  
   1.103  fun instantiation (tycos, vs, sort) thy =
   1.104 @@ -545,7 +545,7 @@
   1.105    in
   1.106      thy
   1.107      |> Theory.checkpoint
   1.108 -    |> ProofContext.init_global
   1.109 +    |> Proof_Context.init_global
   1.110      |> Instantiation.put (mk_instantiation ((tycos, vs, sort), params))
   1.111      |> fold (Variable.declare_typ o TFree) vs
   1.112      |> fold (Variable.declare_names o Free o snd) params
   1.113 @@ -593,8 +593,8 @@
   1.114  
   1.115  fun prove_instantiation_exit_result f tac x lthy =
   1.116    let
   1.117 -    val morph = ProofContext.export_morphism lthy
   1.118 -      (ProofContext.init_global (ProofContext.theory_of lthy));
   1.119 +    val morph = Proof_Context.export_morphism lthy
   1.120 +      (Proof_Context.init_global (Proof_Context.theory_of lthy));
   1.121      val y = f morph x;
   1.122    in
   1.123      lthy
   1.124 @@ -610,11 +610,11 @@
   1.125      val (tycos, vs, sort) = read_multi_arity thy raw_arities;
   1.126      val sorts = map snd vs;
   1.127      val arities = maps (fn tyco => Logic.mk_arities (tyco, sorts, sort)) tycos;
   1.128 -    fun after_qed results = ProofContext.background_theory
   1.129 +    fun after_qed results = Proof_Context.background_theory
   1.130        ((fold o fold) AxClass.add_arity results);
   1.131    in
   1.132      thy
   1.133 -    |> ProofContext.init_global
   1.134 +    |> Proof_Context.init_global
   1.135      |> Proof.theorem NONE after_qed (map (fn t => [(t, [])]) arities)
   1.136    end;
   1.137