Display.pretty_thm_sg;
authorwenzelm
Sun Sep 17 22:21:31 2000 +0200 (2000-09-17)
changeset 1000861eb9f3aa92a
parent 10007 64bf7da1994a
child 10009 45c1eb3d8ad4
Display.pretty_thm_sg;
src/HOL/Tools/induct_method.ML
src/HOL/Tools/inductive_package.ML
src/HOL/Tools/record_package.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/method.ML
src/Pure/axclass.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/HOL/Tools/induct_method.ML	Sun Sep 17 22:19:02 2000 +0200
     1.2 +++ b/src/HOL/Tools/induct_method.ML	Sun Sep 17 22:21:31 2000 +0200
     1.3 @@ -47,9 +47,9 @@
     1.4  
     1.5  fun lookup_rule (rs:rules) name = Library.assoc (NetRules.rules rs, name);
     1.6  
     1.7 -fun print_rules kind rs =
     1.8 +fun print_rules kind sg rs =
     1.9    let val thms = map snd (NetRules.rules rs)
    1.10 -  in Pretty.writeln (Pretty.big_list kind (map Display.pretty_thm thms)) end;
    1.11 +  in Pretty.writeln (Pretty.big_list kind (map (Display.pretty_thm_sg sg) thms)) end;
    1.12  
    1.13  
    1.14  (* theory data kind 'HOL/induct_method' *)
    1.15 @@ -67,11 +67,11 @@
    1.16      ((NetRules.merge (casesT1, casesT2), NetRules.merge (casesS1, casesS2)),
    1.17        (NetRules.merge (inductT1, inductT2), NetRules.merge (inductS1, inductS2)));
    1.18  
    1.19 -  fun print _ ((casesT, casesS), (inductT, inductS)) =
    1.20 -    (print_rules "type cases:" casesT;
    1.21 -      print_rules "set cases:" casesS;
    1.22 -      print_rules "type induct:" inductT;
    1.23 -      print_rules "set induct:" inductS);
    1.24 +  fun print sg ((casesT, casesS), (inductT, inductS)) =
    1.25 +    (print_rules "type cases:" sg casesT;
    1.26 +      print_rules "set cases:" sg casesS;
    1.27 +      print_rules "type induct:" sg inductT;
    1.28 +      print_rules "set induct:" sg inductS);
    1.29  
    1.30    fun dest ((casesT, casesS), (inductT, inductS)) =
    1.31      {type_cases = NetRules.rules casesT,
    1.32 @@ -93,7 +93,7 @@
    1.33    type T = GlobalInductArgs.T;
    1.34  
    1.35    fun init thy = GlobalInduct.get thy;
    1.36 -  fun print x = GlobalInductArgs.print x;
    1.37 +  val print = GlobalInductArgs.print o ProofContext.sign_of;
    1.38  end;
    1.39  
    1.40  structure LocalInduct = ProofDataFun(LocalInductArgs);
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Sun Sep 17 22:19:02 2000 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Sun Sep 17 22:21:31 2000 +0200
     2.3 @@ -81,7 +81,7 @@
     2.4  
     2.5    fun print sg (tab, monos) =
     2.6      [Pretty.strs ("(co)inductives:" :: map #1 (Sign.cond_extern_table sg Sign.constK tab)),
     2.7 -     Pretty.big_list "monotonicity rules:" (map Display.pretty_thm monos)]
     2.8 +     Pretty.big_list "monotonicity rules:" (map (Display.pretty_thm_sg sg) monos)]
     2.9      |> Pretty.chunks |> Pretty.writeln;
    2.10  end;
    2.11  
     3.1 --- a/src/HOL/Tools/record_package.ML	Sun Sep 17 22:19:02 2000 +0200
     3.2 +++ b/src/HOL/Tools/record_package.ML	Sun Sep 17 22:21:31 2000 +0200
     3.3 @@ -828,8 +828,8 @@
     3.4            ("make_defs", make_defs),
     3.5            ("select_convs", sel_convs),
     3.6            ("update_convs", update_convs)]
     3.7 -      |> (#1 oo (PureThy.add_thms o map Thm.no_attributes))
     3.8 -          [("equality", equality)]
     3.9 +      |> (#1 oo PureThy.add_thms)
    3.10 +          [(("equality", equality), [Classical.xtra_intro_global])]
    3.11        |> (#1 oo PureThy.add_thmss)
    3.12          [(("simps", simps), [Simplifier.simp_add_global]),
    3.13           (("iffs", iffs), [iff_add_global])];
     4.1 --- a/src/Pure/Isar/calculation.ML	Sun Sep 17 22:19:02 2000 +0200
     4.2 +++ b/src/Pure/Isar/calculation.ML	Sun Sep 17 22:21:31 2000 +0200
     4.3 @@ -28,8 +28,8 @@
     4.4  
     4.5  (* theory data kind 'Isar/calculation' *)
     4.6  
     4.7 -fun print_rules rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
     4.8 -  (map Display.pretty_thm (NetRules.rules rs)));
     4.9 +fun print_rules sg rs = Pretty.writeln (Pretty.big_list "transitivity rules:"
    4.10 +  (map (Display.pretty_thm_sg sg) (NetRules.rules rs)));
    4.11  
    4.12  structure GlobalCalculationArgs =
    4.13  struct
    4.14 @@ -40,7 +40,7 @@
    4.15    val copy = I;
    4.16    val prep_ext = I;
    4.17    val merge = NetRules.merge;
    4.18 -  fun print _ = print_rules;
    4.19 +  val print = print_rules;
    4.20  end;
    4.21  
    4.22  structure GlobalCalculation = TheoryDataFun(GlobalCalculationArgs);
    4.23 @@ -55,7 +55,7 @@
    4.24    type T = thm NetRules.T * (thm list * int) option;
    4.25  
    4.26    fun init thy = (GlobalCalculation.get thy, None);
    4.27 -  fun print _ (rs, _) = print_rules rs;
    4.28 +  fun print ctxt (rs, _) = print_rules (ProofContext.sign_of ctxt) rs;
    4.29  end;
    4.30  
    4.31  structure LocalCalculation = ProofDataFun(LocalCalculationArgs);
     5.1 --- a/src/Pure/Isar/method.ML	Sun Sep 17 22:19:02 2000 +0200
     5.2 +++ b/src/Pure/Isar/method.ML	Sun Sep 17 22:21:31 2000 +0200
     5.3 @@ -127,11 +127,14 @@
     5.4  
     5.5  (** global and local rule data **)
     5.6  
     5.7 -fun prt_rules kind ths =
     5.8 -  Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:") (map Display.pretty_thm ths));
     5.9 -
    5.10 -fun print_rules (intro, elim) =
    5.11 -  (prt_rules "introduction" intro; prt_rules "elimination" elim);
    5.12 +local
    5.13 +  fun prt_rules kind sg ths =
    5.14 +    Pretty.writeln (Pretty.big_list ("standard " ^ kind ^ " rules:")
    5.15 +      (map (Display.pretty_thm_sg sg) ths));
    5.16 +in
    5.17 +  fun print_rules sg (intro, elim) =
    5.18 +    (prt_rules "introduction" sg intro; prt_rules "elimination" sg elim);
    5.19 +end;
    5.20  
    5.21  
    5.22  (* theory data kind 'Isar/rules' *)
    5.23 @@ -146,7 +149,7 @@
    5.24    val prep_ext = I;
    5.25    fun merge ((intro1, elim1), (intro2, elim2)) =
    5.26      (Drule.merge_rules (intro1, intro2), Drule.merge_rules (elim1, elim2));
    5.27 -  fun print _ = print_rules;
    5.28 +  val print = print_rules;
    5.29  end;
    5.30  
    5.31  structure GlobalRules = TheoryDataFun(GlobalRulesArgs);
    5.32 @@ -161,7 +164,7 @@
    5.33    type T = thm list * thm list;
    5.34  
    5.35    val init = GlobalRules.get;
    5.36 -  fun print _ = print_rules;
    5.37 +  val print = print_rules o ProofContext.sign_of;
    5.38  end;
    5.39  
    5.40  structure LocalRules = ProofDataFun(LocalRulesArgs);
     6.1 --- a/src/Pure/axclass.ML	Sun Sep 17 22:19:02 2000 +0200
     6.2 +++ b/src/Pure/axclass.ML	Sun Sep 17 22:21:31 2000 +0200
     6.3 @@ -189,7 +189,8 @@
     6.4          (Pretty.str (ext_class c) :: Pretty.str " <" :: Pretty.brk 1 ::
     6.5            Pretty.breaks (map (Pretty.str o ext_class) cs));
     6.6  
     6.7 -      fun pretty_thms name thms = Pretty.big_list (name ^ ":") (map Display.pretty_thm thms);
     6.8 +      fun pretty_thms name thms = Pretty.big_list (name ^ ":")
     6.9 +        (map (Display.pretty_thm_sg sg) thms);
    6.10  
    6.11        fun pretty_axclass (name, {super_classes, intro, axioms}) = Pretty.block (Pretty.fbreaks
    6.12          [pretty_class name super_classes, pretty_thms introN [intro], pretty_thms axiomsN axioms]);
     7.1 --- a/src/Pure/pure_thy.ML	Sun Sep 17 22:19:02 2000 +0200
     7.2 +++ b/src/Pure/pure_thy.ML	Sun Sep 17 22:21:31 2000 +0200
     7.3 @@ -87,7 +87,7 @@
     7.4  
     7.5    fun pretty sg (ref {space, thms_tab, const_idx = _}) =
     7.6      let
     7.7 -      val prt_thm = Display.pretty_thm o Thm.transfer_sg sg;
     7.8 +      val prt_thm = Display.pretty_thm_sg sg;
     7.9        fun prt_thms (name, [th]) =
    7.10              Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    7.11          | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    7.12 @@ -213,7 +213,8 @@
    7.13  fun thms_containing thy consts =
    7.14    (case filter (is_none o Sign.const_type (Theory.sign_of thy)) consts of
    7.15      [] => flat (map (containing consts) (thy :: Theory.ancestors_of thy))
    7.16 -  | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]));
    7.17 +  | cs => raise THEORY ("thms_containing: undeclared consts " ^ commas_quote cs, [thy]))
    7.18 +  |> map (apsnd (Thm.transfer thy));
    7.19  
    7.20  
    7.21