src/Pure/Isar/class.ML
changeset 42359 6ca5407863ed
parent 41270 dea60d052923
child 42360 da8817d01e7c
     1.1 --- a/src/Pure/Isar/class.ML	Sat Apr 16 13:48:45 2011 +0200
     1.2 +++ b/src/Pure/Isar/class.ML	Sat Apr 16 15:25:25 2011 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4    val these_defs: theory -> sort -> thm list
     1.5    val these_operations: theory -> sort
     1.6      -> (string * (class * (typ * term))) list
     1.7 -  val print_classes: theory -> unit
     1.8 +  val print_classes: Proof.context -> unit
     1.9    val init: class -> theory -> Proof.context
    1.10    val begin: class list -> sort -> Proof.context -> Proof.context
    1.11    val const: class -> (binding * mixfix) * (term list * term) -> local_theory -> local_theory
    1.12 @@ -69,7 +69,7 @@
    1.13    assm_intro: thm option,
    1.14    of_class: thm,
    1.15    axiom: thm option,
    1.16 -  
    1.17 +
    1.18    (* dynamic part *)
    1.19    defs: thm list,
    1.20    operations: (string * (class * (typ * term))) list
    1.21 @@ -149,9 +149,9 @@
    1.22    | NONE => base_morphism thy class;
    1.23  val export_morphism = #export_morph oo the_class_data;
    1.24  
    1.25 -fun print_classes thy =
    1.26 +fun print_classes ctxt =
    1.27    let
    1.28 -    val ctxt = ProofContext.init_global thy;
    1.29 +    val thy = ProofContext.theory_of ctxt;
    1.30      val algebra = Sign.classes_of thy;
    1.31      val arities =
    1.32        Symtab.empty
    1.33 @@ -163,10 +163,11 @@
    1.34        let
    1.35          val Ss = Sorts.mg_domain algebra tyco [class];
    1.36        in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
    1.37 -    fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
    1.38 -      ^ (Syntax.string_of_typ (Config.put show_sorts false ctxt) o Type.strip_sorts) ty);
    1.39 +    fun mk_param (c, ty) =
    1.40 +      Pretty.str (ProofContext.extern_const ctxt c ^ " :: " ^
    1.41 +        Syntax.string_of_typ (Config.put show_sorts false ctxt) (Type.strip_sorts ty));
    1.42      fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
    1.43 -      (SOME o Pretty.str) ("class " ^ Sign.extern_class thy class ^ ":"),
    1.44 +      (SOME o Pretty.str) ("class " ^ ProofContext.extern_class ctxt class ^ ":"),
    1.45        (SOME o Pretty.block) [Pretty.str "supersort: ",
    1.46          (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
    1.47        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks)
    1.48 @@ -500,18 +501,20 @@
    1.49      val thy = ProofContext.theory_of lthy;
    1.50      fun pr_arity tyco = Syntax.pretty_arity lthy (tyco, map snd vs, sort);
    1.51      fun pr_param ((c, _), (v, ty)) =
    1.52 -      (Pretty.block o Pretty.breaks) [Pretty.str v, Pretty.str "==",
    1.53 -        (Pretty.str o Sign.extern_const thy) c, Pretty.str "::", Syntax.pretty_typ_global thy ty];
    1.54 +      Pretty.block (Pretty.breaks
    1.55 +        [Pretty.str v, Pretty.str "==", Pretty.str (ProofContext.extern_const lthy c),
    1.56 +          Pretty.str "::", Syntax.pretty_typ lthy ty]);
    1.57    in Pretty.str "instantiation" :: map pr_arity tycos @ map pr_param params end;
    1.58  
    1.59  fun conclude lthy =
    1.60    let
    1.61 -    val (tycos, vs, sort) = (#arities o the_instantiation) lthy;
    1.62 +    val (tycos, vs, sort) = #arities (the_instantiation lthy);
    1.63      val thy = ProofContext.theory_of lthy;
    1.64 -    val _ = map (fn tyco => if Sign.of_sort thy
    1.65 +    val _ = tycos |> List.app (fn tyco =>
    1.66 +      if Sign.of_sort thy
    1.67          (Type (tyco, map TFree vs), sort)
    1.68 -      then () else error ("Missing instance proof for type " ^ quote (Sign.extern_type thy tyco)))
    1.69 -        tycos;
    1.70 +      then ()
    1.71 +      else error ("Missing instance proof for type " ^ quote (ProofContext.extern_type lthy tyco)));
    1.72    in lthy end;
    1.73  
    1.74  fun instantiation (tycos, vs, sort) thy =