eliminated tthm type and Attribute structure;
authorwenzelm
Tue Jan 12 13:40:08 1999 +0100 (1999-01-12)
changeset 6091e3cdbd929a24
parent 6090 78c068b838ff
child 6092 d9db67970c73
eliminated tthm type and Attribute structure;
src/Pure/Isar/attrib.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_thy.ML
src/Pure/Isar/method.ML
src/Pure/Isar/proof.ML
src/Pure/Isar/proof_context.ML
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/Isar/attrib.ML	Tue Jan 12 13:39:41 1999 +0100
     1.2 +++ b/src/Pure/Isar/attrib.ML	Tue Jan 12 13:40:08 1999 +0100
     1.3 @@ -21,12 +21,12 @@
     1.4    val local_attribute': Proof.context -> Args.src -> Proof.context attribute
     1.5    val add_attributes: (bstring * ((Args.src -> theory attribute) *
     1.6        (Args.src -> Proof.context attribute)) * string) list -> theory -> theory
     1.7 -  val global_thm: theory * Args.T list -> tthm * (theory * Args.T list)
     1.8 -  val global_thms: theory * Args.T list -> tthm list * (theory * Args.T list)
     1.9 -  val global_thmss: theory * Args.T list -> tthm list * (theory * Args.T list)
    1.10 -  val local_thm: Proof.context * Args.T list -> tthm * (Proof.context * Args.T list)
    1.11 -  val local_thms: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
    1.12 -  val local_thmss: Proof.context * Args.T list -> tthm list * (Proof.context * Args.T list)
    1.13 +  val global_thm: theory * Args.T list -> thm * (theory * Args.T list)
    1.14 +  val global_thms: theory * Args.T list -> thm list * (theory * Args.T list)
    1.15 +  val global_thmss: theory * Args.T list -> thm list * (theory * Args.T list)
    1.16 +  val local_thm: Proof.context * Args.T list -> thm * (Proof.context * Args.T list)
    1.17 +  val local_thms: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    1.18 +  val local_thmss: Proof.context * Args.T list -> thm list * (Proof.context * Args.T list)
    1.19    val syntax: ('a * Args.T list -> 'a attribute * ('a * Args.T list)) -> Args.src -> 'a attribute
    1.20    val no_args: 'a attribute -> Args.src -> 'a attribute
    1.21    val setup: (theory -> theory) list
    1.22 @@ -127,12 +127,12 @@
    1.23    Scan.depend (fn st => Args.name -- Args.opt_attribs >>
    1.24      (fn (name, srcs) => app ((st, get st name), map (attrib st) srcs)));
    1.25  
    1.26 -val global_thm = gen_thm PureThy.get_tthm global_attribute Attribute.apply;
    1.27 -val global_thms = gen_thm PureThy.get_tthms global_attribute Attribute.applys;
    1.28 +val global_thm = gen_thm PureThy.get_thm global_attribute Thm.apply_attributes;
    1.29 +val global_thms = gen_thm PureThy.get_thms global_attribute Thm.applys_attributes;
    1.30  val global_thmss = Scan.repeat global_thms >> flat;
    1.31  
    1.32 -val local_thm = gen_thm ProofContext.get_tthm local_attribute' Attribute.apply;
    1.33 -val local_thms = gen_thm ProofContext.get_tthms local_attribute' Attribute.applys;
    1.34 +val local_thm = gen_thm ProofContext.get_thm local_attribute' Thm.apply_attributes;
    1.35 +val local_thms = gen_thm ProofContext.get_thms local_attribute' Thm.applys_attributes;
    1.36  val local_thmss = Scan.repeat local_thms >> flat;
    1.37  
    1.38  
    1.39 @@ -151,13 +151,13 @@
    1.40  
    1.41  (* tags *)
    1.42  
    1.43 -fun gen_tag x = syntax (tag >> Attribute.tag) x;
    1.44 -fun gen_untag x = syntax (tag >> Attribute.untag) x;
    1.45 +fun gen_tag x = syntax (tag >> Drule.tag) x;
    1.46 +fun gen_untag x = syntax (tag >> Drule.untag) x;
    1.47  
    1.48  
    1.49  (* transfer *)
    1.50  
    1.51 -fun gen_transfer theory_of = no_args (Attribute.rule (fn st => Thm.transfer (theory_of st)));
    1.52 +fun gen_transfer theory_of = no_args (Drule.rule_attribute (fn st => Thm.transfer (theory_of st)));
    1.53  
    1.54  val global_transfer = gen_transfer I;
    1.55  val local_transfer = gen_transfer ProofContext.theory_of;
    1.56 @@ -165,8 +165,7 @@
    1.57  
    1.58  (* RS *)
    1.59  
    1.60 -fun resolve (i, B) (x, A) =
    1.61 -  (x, Attribute.tthm_of (Attribute.thm_of A RSN (i, Attribute.thm_of B)));
    1.62 +fun resolve (i, B) (x, A) = (x, A RSN (i, B));
    1.63  
    1.64  fun gen_RS thm = syntax (Scan.lift (Scan.optional Args.nat 1) -- thm >> resolve);
    1.65  val global_RS = gen_RS global_thm;
    1.66 @@ -175,8 +174,7 @@
    1.67  
    1.68  (* APP *)
    1.69  
    1.70 -fun apply Bs (x, A) =
    1.71 -  (x, Attribute.tthm_of (Attribute.thms_of Bs MRS Attribute.thm_of A));
    1.72 +fun apply Bs (x, A) = (x, Bs MRS A);
    1.73  
    1.74  val global_APP = syntax (global_thmss >> apply);
    1.75  val local_APP = syntax (local_thmss >> apply);
    1.76 @@ -207,7 +205,7 @@
    1.77  
    1.78  fun insts x = Scan.lift (Args.enum "and" (Args.var --| Args.$$$ "=" -- Args.name)) x;
    1.79  
    1.80 -fun gen_where context_of = syntax (insts >> (Attribute.rule o read_instantiate context_of));
    1.81 +fun gen_where context_of = syntax (insts >> (Drule.rule_attribute o read_instantiate context_of));
    1.82  
    1.83  val global_where = gen_where ProofContext.init;
    1.84  val local_where = gen_where I;
    1.85 @@ -231,7 +229,7 @@
    1.86  val inst_args = Scan.repeat inst_arg;
    1.87  fun insts' x = Scan.lift (inst_args -- Scan.optional (concl |-- Args.!!! inst_args) []) x;
    1.88  
    1.89 -fun gen_with context_of = syntax (insts' >> (Attribute.rule o read_instantiate' context_of));
    1.90 +fun gen_with context_of = syntax (insts' >> (Drule.rule_attribute o read_instantiate' context_of));
    1.91  
    1.92  val global_with = gen_with ProofContext.init;
    1.93  val local_with = gen_with I;
    1.94 @@ -239,8 +237,8 @@
    1.95  
    1.96  (* misc rules *)
    1.97  
    1.98 -fun standard x = no_args (Attribute.rule (K Drule.standard)) x;
    1.99 -fun elimify x = no_args (Attribute.rule (K Tactic.make_elim)) x;
   1.100 +fun standard x = no_args (Drule.rule_attribute (K Drule.standard)) x;
   1.101 +fun elimify x = no_args (Drule.rule_attribute (K Tactic.make_elim)) x;
   1.102  
   1.103  
   1.104  
     2.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jan 12 13:39:41 1999 +0100
     2.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jan 12 13:40:08 1999 +0100
     2.3 @@ -98,19 +98,19 @@
     2.4  (* print theorems *)
     2.5  
     2.6  fun global_attribs thy ths srcs =
     2.7 -  #2 (Attribute.applys ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs));
     2.8 +  #2 (Thm.applys_attributes ((Theory.copy thy, ths), map (Attrib.global_attribute thy) srcs));
     2.9  
    2.10  fun local_attribs st ths srcs =
    2.11 -  #2 (Attribute.applys ((Proof.context_of st, ths),
    2.12 +  #2 (Thm.applys_attributes ((Proof.context_of st, ths),
    2.13      map (Attrib.local_attribute (Proof.theory_of st)) srcs));
    2.14  
    2.15  fun print_thms (name, srcs) = Toplevel.keep (fn state =>
    2.16    let
    2.17 -    val ths = map (apfst (Thm.transfer (Toplevel.theory_of state)))
    2.18 -      (Toplevel.node_cases PureThy.get_tthms (ProofContext.get_tthms o Proof.context_of)
    2.19 +    val ths = map (Thm.transfer (Toplevel.theory_of state))
    2.20 +      (Toplevel.node_cases PureThy.get_thms (ProofContext.get_thms o Proof.context_of)
    2.21          state name);
    2.22      val ths' = Toplevel.node_cases global_attribs local_attribs state ths srcs;
    2.23 -  in Attribute.print_tthms ths' end);
    2.24 +  in Display.print_thms ths' end);
    2.25  
    2.26  
    2.27  (* print types, terms and props *)
     3.1 --- a/src/Pure/Isar/isar_thy.ML	Tue Jan 12 13:39:41 1999 +0100
     3.2 +++ b/src/Pure/Isar/isar_thy.ML	Tue Jan 12 13:40:08 1999 +0100
     3.3 @@ -94,16 +94,16 @@
     3.4  
     3.5  
     3.6  val have_theorems =
     3.7 -  #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute PureThy.have_tthmss;
     3.8 +  #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute PureThy.have_thmss;
     3.9  
    3.10  val have_lemmas =
    3.11 -  #1 oo gen_have_thmss PureThy.get_tthms Attrib.global_attribute
    3.12 -    (fn name => fn more_atts => PureThy.have_tthmss name (more_atts @ [Attribute.tag_lemma]));
    3.13 +  #1 oo gen_have_thmss PureThy.get_thms Attrib.global_attribute
    3.14 +    (fn name => fn more_atts => PureThy.have_thmss name (more_atts @ [Drule.tag_lemma]));
    3.15  
    3.16  
    3.17  val have_thmss =
    3.18 -  gen_have_thmss (ProofContext.get_tthms o Proof.context_of)
    3.19 -    (Attrib.local_attribute o Proof.theory_of) Proof.have_tthmss;
    3.20 +  gen_have_thmss (ProofContext.get_thms o Proof.context_of)
    3.21 +    (Attrib.local_attribute o Proof.theory_of) Proof.have_thmss;
    3.22  
    3.23  val have_facts = ProofHistory.apply o have_thmss;
    3.24  val from_facts = ProofHistory.apply o (Proof.chain oo curry have_thmss ("", []));
    3.25 @@ -143,10 +143,10 @@
    3.26      val state = ProofHistory.current prf;
    3.27      val thy = Proof.theory_of state;
    3.28      val alt_atts = apsome (map (Attrib.global_attribute thy)) alt_tags;
    3.29 -    val (thy', (kind, name, tthm)) = Method.qed alt_name alt_atts state;
    3.30 +    val (thy', (kind, name, thm)) = Method.qed alt_name alt_atts state;
    3.31  
    3.32      val prt_result = Pretty.block
    3.33 -      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Attribute.pretty_tthm tthm];
    3.34 +      [Pretty.str (kind ^ " " ^ name ^ ":"), Pretty.fbrk, Display.pretty_thm thm];
    3.35    in Pretty.writeln prt_result; thy end;
    3.36  
    3.37  val qed = qed_with (None, None);
     4.1 --- a/src/Pure/Isar/method.ML	Tue Jan 12 13:39:41 1999 +0100
     4.2 +++ b/src/Pure/Isar/method.ML	Tue Jan 12 13:40:08 1999 +0100
     4.3 @@ -14,16 +14,16 @@
     4.4  signature METHOD =
     4.5  sig
     4.6    include BASIC_METHOD
     4.7 -  val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * tthm list) list) Seq.seq
     4.8 -  val METHOD: (tthm list -> tactic) -> Proof.method
     4.9 +  val LIFT: tactic -> thm -> (thm * (indexname * term) list * (string * thm list) list) Seq.seq
    4.10 +  val METHOD: (thm list -> tactic) -> Proof.method
    4.11    val METHOD0: tactic -> Proof.method
    4.12    val fail: Proof.method
    4.13    val succeed: Proof.method
    4.14    val trivial: Proof.method
    4.15    val assumption: Proof.method
    4.16    val forward_chain: thm list -> thm list -> thm Seq.seq
    4.17 -  val rule_tac: tthm list -> tthm list -> int -> tactic
    4.18 -  val rule: tthm list -> Proof.method
    4.19 +  val rule_tac: thm list -> thm list -> int -> tactic
    4.20 +  val rule: thm list -> Proof.method
    4.21    exception METHOD_FAIL of (string * Position.T) * exn
    4.22    val method: theory -> Args.src -> Proof.context -> Proof.method
    4.23    val add_methods: (bstring * (Args.src -> Proof.context -> Proof.method) * string) list
    4.24 @@ -40,7 +40,7 @@
    4.25      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    4.26    val only_sectioned_args: (Args.T list -> Proof.context attribute * Args.T list) list ->
    4.27      (Proof.context -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    4.28 -  val thms_args: (tthm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    4.29 +  val thms_args: (thm list -> Proof.method) -> Args.src -> Proof.context -> Proof.method
    4.30    datatype text =
    4.31      Basic of (Proof.context -> Proof.method) |
    4.32      Source of Args.src |
    4.33 @@ -59,7 +59,7 @@
    4.34    val trivial_proof: Proof.state -> Proof.state Seq.seq
    4.35    val default_proof: Proof.state -> Proof.state Seq.seq
    4.36    val qed: bstring option -> theory attribute list option -> Proof.state
    4.37 -    -> theory * (string * string * tthm)
    4.38 +    -> theory * (string * string * thm)
    4.39    val setup: (theory -> theory) list
    4.40  end;
    4.41  
    4.42 @@ -86,10 +86,8 @@
    4.43  
    4.44  fun trivial_tac [] = K all_tac
    4.45    | trivial_tac facts =
    4.46 -      let
    4.47 -        val thms = Attribute.thms_of facts;
    4.48 -        val r = ~ (length facts);
    4.49 -      in metacuts_tac thms THEN' rotate_tac r end;
    4.50 +      let val r = ~ (length facts);
    4.51 +      in metacuts_tac facts THEN' rotate_tac r end;
    4.52  
    4.53  val trivial = METHOD (ALLGOALS o trivial_tac);
    4.54  val assumption = METHOD (fn facts => FIRSTGOAL (trivial_tac facts THEN' assume_tac));
    4.55 @@ -109,10 +107,10 @@
    4.56  
    4.57  fun forward_chain facts rules = Seq.flat (Seq.map (multi_resolve facts) (Seq.of_list rules));
    4.58  
    4.59 -fun rule_tac rules [] = resolve_tac (Attribute.thms_of rules)
    4.60 +fun rule_tac rules [] = resolve_tac rules
    4.61    | rule_tac erules facts =
    4.62        let
    4.63 -        val rules = forward_chain (Attribute.thms_of facts) (Attribute.thms_of erules);
    4.64 +        val rules = forward_chain facts erules;
    4.65          fun tac i state = Seq.flat (Seq.map (fn rule => Tactic.rtac rule i state) rules);
    4.66        in tac end;
    4.67  
    4.68 @@ -209,7 +207,7 @@
    4.69  fun thms ss = Scan.unless (sect ss) Attrib.local_thms;
    4.70  fun thmss ss = Scan.repeat (thms ss) >> flat;
    4.71  
    4.72 -fun apply att (ctxt, ths) = Attribute.applys ((ctxt, ths), [att]);
    4.73 +fun apply att (ctxt, ths) = Thm.applys_attributes ((ctxt, ths), [att]);
    4.74  
    4.75  fun section ss = (sect ss -- thmss ss) :-- (fn (att, ths) => Scan.depend (fn ctxt =>
    4.76    Scan.succeed (apply att (ctxt, ths)))) >> #2;
     5.1 --- a/src/Pure/Isar/proof.ML	Tue Jan 12 13:39:41 1999 +0100
     5.2 +++ b/src/Pure/Isar/proof.ML	Tue Jan 12 13:40:08 1999 +0100
     5.3 @@ -22,23 +22,23 @@
     5.4    val context_of: state -> context
     5.5    val theory_of: state -> theory
     5.6    val sign_of: state -> Sign.sg
     5.7 -  val the_facts: state -> tthm list
     5.8 -  val goal_facts: (state -> tthm list) -> state -> state
     5.9 +  val the_facts: state -> thm list
    5.10 +  val goal_facts: (state -> thm list) -> state -> state
    5.11    val use_facts: state -> state
    5.12    val reset_facts: state -> state
    5.13    val assert_backward: state -> state
    5.14    val enter_forward: state -> state
    5.15    val print_state: state -> unit
    5.16    type method
    5.17 -  val method: (tthm list -> thm ->
    5.18 -    (thm * (indexname * term) list * (string * tthm list) list) Seq.seq) -> method
    5.19 +  val method: (thm list -> thm ->
    5.20 +    (thm * (indexname * term) list * (string * thm list) list) Seq.seq) -> method
    5.21    val refine: (context -> method) -> state -> state Seq.seq
    5.22    val bind: (indexname * string) list -> state -> state
    5.23    val bind_i: (indexname * term) list -> state -> state
    5.24    val match_bind: (string list * string) list -> state -> state
    5.25    val match_bind_i: (term list * term) list -> state -> state
    5.26 -  val have_tthmss: string -> context attribute list ->
    5.27 -    (tthm list * context attribute list) list -> state -> state
    5.28 +  val have_thmss: string -> context attribute list ->
    5.29 +    (thm list * context attribute list) list -> state -> state
    5.30    val assume: string -> context attribute list -> (string * string list) list -> state -> state
    5.31    val assume_i: string -> context attribute list -> (term * term list) list -> state -> state
    5.32    val fix: (string * string option) list -> state -> state
    5.33 @@ -48,7 +48,7 @@
    5.34    val lemma: bstring -> theory attribute list -> string * string list -> theory -> state
    5.35    val lemma_i: bstring -> theory attribute list -> term * term list -> theory -> state
    5.36    val chain: state -> state
    5.37 -  val from_facts: tthm list -> state -> state
    5.38 +  val from_facts: thm list -> state -> state
    5.39    val show: string -> context attribute list -> string * string list -> state -> state
    5.40    val show_i: string -> context attribute list -> term * term list -> state -> state
    5.41    val have: string -> context attribute list -> string * string list -> state -> state
    5.42 @@ -57,7 +57,7 @@
    5.43    val next_block: state -> state
    5.44    val end_block: (context -> method) -> state -> state Seq.seq
    5.45    val qed: (context -> method) -> bstring option -> theory attribute list option -> state
    5.46 -    -> theory * (string * string * tthm)
    5.47 +    -> theory * (string * string * thm)
    5.48  end;
    5.49  
    5.50  signature PROOF_PRIVATE =
    5.51 @@ -87,11 +87,11 @@
    5.52    fn Theorem _ => "theorem" | Lemma _ => "lemma" | Goal _ => "show" | Aux _ => "have";
    5.53  
    5.54  type goal =
    5.55 - (kind *		(*result kind*)
    5.56 + (kind *                (*result kind*)
    5.57    string *              (*result name*)
    5.58    cterm list *          (*result assumptions*)
    5.59    term) *               (*result statement*)
    5.60 - (tthm list *           (*use facts*)
    5.61 + (thm list *            (*use facts*)
    5.62    thm);                 (*goal: subgoals ==> statement*)
    5.63  
    5.64  
    5.65 @@ -107,7 +107,7 @@
    5.66  
    5.67  type node =
    5.68   {context: context,
    5.69 -  facts: tthm list option,
    5.70 +  facts: thm list option,
    5.71    mode: mode,
    5.72    goal: goal option};
    5.73  
    5.74 @@ -154,8 +154,8 @@
    5.75  fun put_data kind f = map_context o ProofContext.put_data kind f;
    5.76  val declare_term = map_context o ProofContext.declare_term;
    5.77  val add_binds = map_context o ProofContext.add_binds_i;
    5.78 -val put_tthms = map_context o ProofContext.put_tthms;
    5.79 -val put_tthmss = map_context o ProofContext.put_tthmss;
    5.80 +val put_thms = map_context o ProofContext.put_thms;
    5.81 +val put_thmss = map_context o ProofContext.put_thmss;
    5.82  
    5.83  
    5.84  (* bind statements *)
    5.85 @@ -164,19 +164,19 @@
    5.86    let val mk_bind = map (fn (x, t) => ((Syntax.binding x, 0), t)) o ObjectLogic.dest_statement
    5.87    in state |> add_binds (flat (map mk_bind bs)) end;
    5.88  
    5.89 -fun bind_tthms (name, tthms) state =
    5.90 +fun bind_thms (name, thms) state =
    5.91    let
    5.92 -    val props = map (#prop o Thm.rep_thm o Attribute.thm_of) tthms;
    5.93 +    val props = map (#prop o Thm.rep_thm) thms;
    5.94      val named_props =
    5.95        (case props of
    5.96          [prop] => [(name, prop)]
    5.97        | props => map2 (fn (i, t) => (name ^ string_of_int i, t)) (1 upto length props, props));
    5.98    in state |> bind_props named_props end;
    5.99  
   5.100 -fun let_tthms name_tthms state =
   5.101 +fun let_thms name_thms state =
   5.102    state
   5.103 -  |> put_tthms name_tthms
   5.104 -  |> bind_tthms name_tthms;
   5.105 +  |> put_thms name_thms
   5.106 +  |> bind_thms name_thms;
   5.107  
   5.108  
   5.109  (* facts *)
   5.110 @@ -187,14 +187,14 @@
   5.111  fun put_facts facts state =
   5.112    state
   5.113    |> map_current (fn (ctxt, _, mode, goal) => (ctxt, facts, mode, goal))
   5.114 -  |> let_tthms ("facts", if_none facts []);
   5.115 +  |> let_thms ("facts", if_none facts []);
   5.116  
   5.117  val reset_facts = put_facts None;
   5.118  
   5.119  fun have_facts (name, facts) state =
   5.120    state
   5.121    |> put_facts (Some facts)
   5.122 -  |> let_tthms (name, facts);
   5.123 +  |> let_thms (name, facts);
   5.124  
   5.125  fun these_facts (state, ths) = have_facts ths state;
   5.126  fun fetch_facts (State ({facts, ...}, _)) = put_facts facts;
   5.127 @@ -266,20 +266,19 @@
   5.128  fun print_state (state as State ({context, facts, mode, goal = _}, nodes)) =
   5.129    let
   5.130      val ref (_, _, begin_goal) = Goals.current_goals_markers;
   5.131 -    val prt_tthm = Attribute.pretty_tthm;
   5.132  
   5.133      fun print_facts None = ()
   5.134        | print_facts (Some ths) =
   5.135 -          Pretty.writeln (Pretty.big_list "Current facts:" (map prt_tthm ths));
   5.136 +          Pretty.writeln (Pretty.big_list "Current facts:" (map Display.pretty_thm ths));
   5.137  
   5.138      fun levels_up 0 = ""
   5.139        | levels_up i = " (" ^ string_of_int i ^ " levels up)";
   5.140  
   5.141      fun print_goal (i, ((kind, name, _, _), (_, thm))) =
   5.142 -      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":");	(* FIXME *)
   5.143 +      (writeln (kind_name kind ^ " " ^ quote name ^ levels_up (i div 1) ^ ":"); (* FIXME *)
   5.144          Locale.print_goals_marker begin_goal (! goals_limit) thm);
   5.145    in
   5.146 -    writeln ("Nesting level: " ^ string_of_int (length nodes div 1));	(* FIXME *)
   5.147 +    writeln ("Nesting level: " ^ string_of_int (length nodes div 1));   (* FIXME *)
   5.148      writeln "";
   5.149      writeln (mode_name mode ^ " mode");
   5.150      writeln "";
   5.151 @@ -296,11 +295,11 @@
   5.152  (* datatype method *)
   5.153  
   5.154  datatype method = Method of
   5.155 -  tthm list ->                   	(*use facts*)
   5.156 +  thm list ->                           (*use facts*)
   5.157    thm                                   (*goal: subgoals ==> statement*)
   5.158      -> (thm *                           (*refined goal*)
   5.159         (indexname * term) list *        (*new bindings*)
   5.160 -       (string * tthm list) list)       (*new thms*)
   5.161 +       (string * thm list) list)        (*new thms*)
   5.162           Seq.seq;
   5.163  
   5.164  val method = Method;
   5.165 @@ -322,7 +321,7 @@
   5.166            |> check_sign (sign_of_thm thm')
   5.167            |> map_goal (K (result, (facts, thm')))
   5.168            |> add_binds new_binds
   5.169 -          |> put_tthmss new_thms;
   5.170 +          |> put_thmss new_thms;
   5.171        in Seq.map refn (meth facts thm) end;
   5.172  
   5.173  
   5.174 @@ -429,12 +428,12 @@
   5.175  val match_bind_i = gen_bind ProofContext.match_binds_i;
   5.176  
   5.177  
   5.178 -(* have_tthmss *)
   5.179 +(* have_thmss *)
   5.180  
   5.181 -fun have_tthmss name atts ths_atts state =
   5.182 +fun have_thmss name atts ths_atts state =
   5.183    state
   5.184    |> assert_forward
   5.185 -  |> map_context_result (ProofContext.have_tthmss (PureThy.default_name name) atts ths_atts)
   5.186 +  |> map_context_result (ProofContext.have_thmss (PureThy.default_name name) atts ths_atts)
   5.187    |> these_facts;
   5.188  
   5.189  
   5.190 @@ -457,7 +456,7 @@
   5.191    |> assert_forward
   5.192    |> map_context_result (f (PureThy.default_name name) atts props)
   5.193    |> these_facts
   5.194 -  |> (fn st => let_tthms ("prems", ProofContext.assumptions (context_of st)) st);
   5.195 +  |> (fn st => let_thms ("prems", ProofContext.assumptions (context_of st)) st);
   5.196  
   5.197  val assume = gen_assume ProofContext.assume;
   5.198  val assume_i = gen_assume ProofContext.assume_i;
   5.199 @@ -490,8 +489,7 @@
   5.200        |> opt_block
   5.201        |> map_context_result (fn c => prepp (c, raw_propp));
   5.202  
   5.203 -    val casms = map (#prop o Thm.crep_thm o Attribute.thm_of)
   5.204 -      (ProofContext.assumptions (context_of state'));
   5.205 +    val casms = map (#prop o Thm.crep_thm) (ProofContext.assumptions (context_of state'));
   5.206      val asms = map Thm.term_of casms;
   5.207  
   5.208      val prop = Logic.list_implies (asms, concl);
   5.209 @@ -597,7 +595,7 @@
   5.210    in
   5.211      state
   5.212      |> close_block
   5.213 -    |> have_tthmss name atts [([(result, [])], [])]
   5.214 +    |> have_thmss name atts [Thm.no_attributes [result]]
   5.215      |> opt_solve
   5.216    end;
   5.217  
   5.218 @@ -626,10 +624,10 @@
   5.219      val atts =
   5.220        (case kind of
   5.221          Theorem atts => if_none alt_atts atts
   5.222 -      | Lemma atts => (if_none alt_atts atts) @ [Attribute.tag_lemma]
   5.223 +      | Lemma atts => (if_none alt_atts atts) @ [Drule.tag_lemma]
   5.224        | _ => raise STATE ("No global goal!", state));
   5.225  
   5.226 -    val (thy', result') = PureThy.store_tthm ((name, (result, [])), atts) (theory_of state);
   5.227 +    val (thy', result') = PureThy.store_thm ((name, result), atts) (theory_of state);
   5.228    in (thy', (kind_name kind, name, result')) end;
   5.229  
   5.230  fun qed meth_fun alt_name alt_atts state =
     6.1 --- a/src/Pure/Isar/proof_context.ML	Tue Jan 12 13:39:41 1999 +0100
     6.2 +++ b/src/Pure/Isar/proof_context.ML	Tue Jan 12 13:40:08 1999 +0100
     6.3 @@ -41,21 +41,21 @@
     6.4    val match_binds_i: (term list * term) list -> context -> context
     6.5    val bind_propp: context * (string * string list) -> context * term
     6.6    val bind_propp_i: context * (term * term list) -> context * term
     6.7 -  val thms_closure: context -> xstring -> tthm list option
     6.8 -  val get_tthm: context -> string -> tthm
     6.9 -  val get_tthms: context -> string -> tthm list
    6.10 -  val get_tthmss: context -> string list -> tthm list
    6.11 -  val put_tthm: string * tthm -> context -> context
    6.12 -  val put_tthms: string * tthm list -> context -> context
    6.13 -  val put_tthmss: (string * tthm list) list -> context -> context
    6.14 -  val have_tthmss: string -> context attribute list
    6.15 -    -> (tthm list * context attribute list) list -> context -> context * (string * tthm list)
    6.16 -  val assumptions: context -> tthm list
    6.17 +  val thms_closure: context -> xstring -> thm list option
    6.18 +  val get_thm: context -> string -> thm
    6.19 +  val get_thms: context -> string -> thm list
    6.20 +  val get_thmss: context -> string list -> thm list
    6.21 +  val put_thm: string * thm -> context -> context
    6.22 +  val put_thms: string * thm list -> context -> context
    6.23 +  val put_thmss: (string * thm list) list -> context -> context
    6.24 +  val have_thmss: string -> context attribute list
    6.25 +    -> (thm list * context attribute list) list -> context -> context * (string * thm list)
    6.26 +  val assumptions: context -> thm list
    6.27    val fixed_names: context -> string list
    6.28    val assume: string -> context attribute list -> (string * string list) list -> context
    6.29 -    -> context * (string * tthm list)
    6.30 +    -> context * (string * thm list)
    6.31    val assume_i: string -> context attribute list -> (term * term list) list -> context
    6.32 -    -> context * (string * tthm list)
    6.33 +    -> context * (string * thm list)
    6.34    val fix: (string * string option) list -> context -> context
    6.35    val fix_i: (string * typ) list -> context -> context
    6.36    val setup: (theory -> theory) list
    6.37 @@ -82,10 +82,10 @@
    6.38     {thy: theory,                                (*current theory*)
    6.39      data: Object.T Symtab.table,                (*user data*)
    6.40      asms:
    6.41 -      (string * tthm list) list *               (*assumes: A ==> _*)
    6.42 +      (string * thm list) list *                (*assumes: A ==> _*)
    6.43        ((string * string) list * string list),   (*fixes: !!x. _*)
    6.44      binds: (term * typ) Vartab.table,           (*term bindings*)
    6.45 -    thms: tthm list Symtab.table,               (*local thms*)
    6.46 +    thms: thm list Symtab.table,                (*local thms*)
    6.47      defs:
    6.48        typ Vartab.table *                        (*type constraints*)
    6.49        sort Vartab.table *                       (*default sorts*)
    6.50 @@ -136,7 +136,7 @@
    6.51  (* local theorems *)
    6.52  
    6.53  fun print_thms (Context {thms, ...}) =
    6.54 -  print_items Attribute.pretty_tthm "Local theorems:" (Symtab.dest thms);
    6.55 +  print_items Display.pretty_thm "Local theorems:" (Symtab.dest thms);
    6.56  
    6.57  
    6.58  (* main context *)
    6.59 @@ -146,7 +146,6 @@
    6.60    let
    6.61      val sign = Theory.sign_of thy;
    6.62  
    6.63 -    val term_of_tthm = #prop o Thm.rep_thm o Attribute.thm_of;
    6.64      val prt_term = Sign.pretty_term sign;
    6.65      val prt_typ = Sign.pretty_typ sign;
    6.66      val prt_sort = Sign.pretty_sort sign;
    6.67 @@ -173,7 +172,7 @@
    6.68    in
    6.69      debug Pretty.writeln pretty_thy;
    6.70      Pretty.writeln (Pretty.big_list "Fixed variables:" (map prt_fix (rev fixes)));
    6.71 -    print_items (prt_term o term_of_tthm) "Assumptions:" assumes;
    6.72 +    print_items (prt_term o #prop o Thm.rep_thm) "Assumptions:" assumes;
    6.73      debug print_binds ctxt;
    6.74      debug print_thms ctxt;
    6.75      debug Pretty.writeln (Pretty.big_list "Type constraints:" (map prt_defT (Vartab.dest types)));
    6.76 @@ -550,44 +549,44 @@
    6.77    in get end;
    6.78  
    6.79  
    6.80 -(* get_tthm(s) *)
    6.81 +(* get_thm(s) *)
    6.82  
    6.83 -fun get_tthm (ctxt as Context {thy, thms, ...}) name =
    6.84 +fun get_thm (ctxt as Context {thy, thms, ...}) name =
    6.85    (case Symtab.lookup (thms, name) of
    6.86      Some [th] => th
    6.87    | Some _ => raise CONTEXT ("Single theorem expected: " ^ quote name, ctxt)
    6.88 -  | None => (PureThy.get_tthm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
    6.89 +  | None => (PureThy.get_thm thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
    6.90  
    6.91 -fun get_tthms (ctxt as Context {thy, thms, ...}) name =
    6.92 +fun get_thms (ctxt as Context {thy, thms, ...}) name =
    6.93    (case Symtab.lookup (thms, name) of
    6.94      Some ths => ths
    6.95 -  | None => (PureThy.get_tthms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
    6.96 +  | None => (PureThy.get_thms thy name handle THEORY (msg, _) => raise CONTEXT (msg, ctxt)));
    6.97  
    6.98 -fun get_tthmss ctxt names = flat (map (get_tthms ctxt) names);
    6.99 +fun get_thmss ctxt names = flat (map (get_thms ctxt) names);
   6.100  
   6.101  
   6.102 -(* put_tthm(s) *)
   6.103 +(* put_thm(s) *)
   6.104  
   6.105 -fun put_tthms (name, ths) = map_context
   6.106 +fun put_thms (name, ths) = map_context
   6.107    (fn (thy, data, asms, binds, thms, defs) =>
   6.108      (thy, data, asms, binds, Symtab.update ((name, ths), thms), defs));
   6.109  
   6.110 -fun put_tthm (name, th) = put_tthms (name, [th]);
   6.111 +fun put_thm (name, th) = put_thms (name, [th]);
   6.112  
   6.113 -fun put_tthmss [] ctxt = ctxt
   6.114 -  | put_tthmss (th :: ths) ctxt = ctxt |> put_tthms th |> put_tthmss ths;
   6.115 +fun put_thmss [] ctxt = ctxt
   6.116 +  | put_thmss (th :: ths) ctxt = ctxt |> put_thms th |> put_thmss ths;
   6.117  
   6.118  
   6.119 -(* have_tthmss *)
   6.120 +(* have_thmss *)
   6.121  
   6.122 -fun have_tthmss name more_attrs ths_attrs ctxt =
   6.123 +fun have_thmss name more_attrs ths_attrs ctxt =
   6.124    let
   6.125      fun app ((ct, ths), (th, attrs)) =
   6.126 -      let val (ct', th') = Attribute.applys ((ct, th), attrs @ more_attrs)
   6.127 +      let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
   6.128        in (ct', th' :: ths) end
   6.129      val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
   6.130      val thms = flat (rev rev_thms);
   6.131 -  in (ctxt' |> put_tthms (name, thms), (name, thms)) end;
   6.132 +  in (ctxt' |> put_thms (name, thms), (name, thms)) end;
   6.133  
   6.134  
   6.135  
   6.136 @@ -606,18 +605,18 @@
   6.137      val (ctxt', props) = foldl_map prepp (ctxt, raw_prop_pats);
   6.138      val sign = sign_of ctxt';
   6.139  
   6.140 -    val asms = map (Attribute.tthm_of o Thm.assume o Thm.cterm_of sign) props;
   6.141 +    val asms = map (Thm.assume o Thm.cterm_of sign) props;
   6.142  
   6.143      val ths = map (fn th => ([th], [])) asms;
   6.144 -    val (ctxt'', (_, tthms)) =
   6.145 +    val (ctxt'', (_, thms)) =
   6.146        ctxt'
   6.147 -      |> have_tthmss name (attrs @ [Attribute.tag_assumption]) ths
   6.148 +      |> have_thmss name (attrs @ [Drule.tag_assumption]) ths;
   6.149  
   6.150      val ctxt''' =
   6.151        ctxt''
   6.152        |> map_context (fn (thy, data, (assumes, fixes), binds, thms, defs) =>
   6.153          (thy, data, (assumes @ [(name, asms)], fixes), binds, thms, defs));
   6.154 -  in (ctxt''', (name, tthms)) end;
   6.155 +  in (ctxt''', (name, thms)) end;
   6.156  
   6.157  val assume = gen_assume bind_propp;
   6.158  val assume_i = gen_assume bind_propp_i;
     7.1 --- a/src/Pure/pure_thy.ML	Tue Jan 12 13:39:41 1999 +0100
     7.2 +++ b/src/Pure/pure_thy.ML	Tue Jan 12 13:40:08 1999 +0100
     7.3 @@ -23,18 +23,16 @@
     7.4  signature PURE_THY =
     7.5  sig
     7.6    include BASIC_PURE_THY
     7.7 -  val thms_closure: theory -> xstring -> tthm list option
     7.8 -  val get_tthm: theory -> xstring -> tthm
     7.9 -  val get_tthms: theory -> xstring -> tthm list
    7.10 -  val get_tthmss: theory -> xstring list -> tthm list
    7.11 +  val thms_closure: theory -> xstring -> thm list option
    7.12 +  val get_thmss: theory -> xstring list -> thm list
    7.13    val thms_containing: theory -> string list -> (string * thm) list
    7.14    val default_name: string -> string
    7.15 -  val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm
    7.16 +  val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
    7.17    val smart_store_thm: (bstring * thm) -> thm
    7.18 -  val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory
    7.19 -  val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory
    7.20 -  val have_tthmss: bstring -> theory attribute list ->
    7.21 -    (tthm list * theory attribute list) list -> theory -> theory * tthm list
    7.22 +  val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory
    7.23 +  val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory
    7.24 +  val have_thmss: bstring -> theory attribute list ->
    7.25 +    (thm list * theory attribute list) list -> theory -> theory * thm list
    7.26    val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory
    7.27    val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
    7.28    val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory
    7.29 @@ -68,8 +66,8 @@
    7.30  
    7.31    type T =
    7.32      {space: NameSpace.T,
    7.33 -      thms_tab: tthm list Symtab.table,
    7.34 -      const_idx: int * (int * tthm) list Symtab.table} ref;
    7.35 +      thms_tab: thm list Symtab.table,
    7.36 +      const_idx: int * (int * thm) list Symtab.table} ref;
    7.37  
    7.38    fun mk_empty _ =
    7.39      ref {space = NameSpace.empty, thms_tab = Symtab.empty, const_idx = (0, Symtab.empty)} : T;
    7.40 @@ -80,7 +78,7 @@
    7.41  
    7.42    fun print sg (ref {space, thms_tab, const_idx = _}) =
    7.43      let
    7.44 -      val prt_thm = Attribute.pretty_tthm o apfst (Thm.transfer_sg sg);
    7.45 +      val prt_thm = Display.pretty_thm o Thm.transfer_sg sg;
    7.46        fun prt_thms (name, [th]) =
    7.47              Pretty.block [Pretty.str (name ^ ":"), Pretty.brk 1, prt_thm th]
    7.48          | prt_thms (name, ths) = Pretty.big_list (name ^ ":") (map prt_thm ths);
    7.49 @@ -125,25 +123,22 @@
    7.50  
    7.51  fun lookup_thms name thy = thms_closure_aux thy name;
    7.52  
    7.53 -fun get_tthms thy name =
    7.54 +fun get_thms thy name =
    7.55    (case get_first (lookup_thms name) (thy :: Theory.ancestors_of thy) of
    7.56      None => raise THEORY ("Unknown theorem(s) " ^ quote name, [thy])
    7.57    | Some thms => thms);
    7.58  
    7.59 -fun get_tthm thy name =
    7.60 -  (case get_tthms thy name of
    7.61 +fun get_thm thy name =
    7.62 +  (case get_thms thy name of
    7.63      [thm] => thm
    7.64    | _ => raise THEORY ("Single theorem expected " ^ quote name, [thy]));
    7.65  
    7.66 -fun get_tthmss thy names = flat (map (get_tthms thy) names);
    7.67 -
    7.68 -fun get_thms thy = Attribute.thms_of o get_tthms thy;
    7.69 -fun get_thm thy = Attribute.thm_of o get_tthm thy;
    7.70 +fun get_thmss thy names = flat (map (get_thms thy) names);
    7.71  
    7.72  
    7.73  (* thms_of *)
    7.74  
    7.75 -fun attach_name (thm, _) = (Thm.name_of_thm thm, thm);
    7.76 +fun attach_name thm = (Thm.name_of_thm thm, thm);
    7.77  
    7.78  fun thms_of thy =
    7.79    let val ref {thms_tab, ...} = get_theorems thy in
    7.80 @@ -158,14 +153,14 @@
    7.81  
    7.82  val ignore = ["Trueprop", "all", "==>", "=="];
    7.83  
    7.84 -fun add_const_idx ((next, table), tthm as (thm, _)) =
    7.85 +fun add_const_idx ((next, table), thm) =
    7.86    let
    7.87      val {hyps, prop, ...} = Thm.rep_thm thm;
    7.88      val consts =
    7.89        foldr add_term_consts (hyps, add_term_consts (prop, [])) \\ ignore;
    7.90  
    7.91      fun add (tab, c) =
    7.92 -      Symtab.update ((c, (next, tthm) :: Symtab.lookup_multi (tab, c)), tab);
    7.93 +      Symtab.update ((c, (next, thm) :: Symtab.lookup_multi (tab, c)), tab);
    7.94    in (next + 1, foldl add (table, consts)) end;
    7.95  
    7.96  fun make_const_idx thm_tab =
    7.97 @@ -214,7 +209,7 @@
    7.98  fun name_multi name xs = gen_names (length xs) (default_name name) ~~ xs;
    7.99  
   7.100  
   7.101 -(* enter_tthmx *)
   7.102 +(* enter_thmx *)
   7.103  
   7.104  fun cond_warning name msg = if Sign.base_name name = defaultN then () else warning msg;
   7.105  
   7.106 @@ -224,72 +219,68 @@
   7.107  fun warn_same name =
   7.108    cond_warning name ("Theorem database already contains a copy of " ^ quote name);
   7.109  
   7.110 -fun enter_tthmx sg app_name (bname, tthmx) =
   7.111 +fun enter_thmx sg app_name (bname, thmx) =
   7.112    let
   7.113      val name = Sign.full_name sg bname;
   7.114 -    fun name_tthm (nm, (thm, tgs)) = (Thm.name_thm (nm, thm), tgs);
   7.115 -    val named_tthms = map name_tthm (app_name name tthmx);
   7.116 -
   7.117 -    fun eq_tthm ((th1, _), (th2, _)) = Thm.eq_thm (th1, th2);
   7.118 +    val named_thms = map Thm.name_thm (app_name name thmx);
   7.119  
   7.120      val r as ref {space, thms_tab, const_idx} = get_theorems_sg sg;
   7.121  
   7.122      val overwrite =
   7.123        (case Symtab.lookup (thms_tab, name) of
   7.124          None => false
   7.125 -      | Some tthms' =>
   7.126 -          if length tthms' = length named_tthms andalso forall2 eq_tthm (tthms', named_tthms) then
   7.127 +      | Some thms' =>
   7.128 +          if length thms' = length named_thms andalso forall2 Thm.eq_thm (thms', named_thms) then
   7.129              (warn_same name; false)
   7.130            else (warn_overwrite name; true));
   7.131  
   7.132      val space' = NameSpace.extend (space, [name]);
   7.133 -    val thms_tab' = Symtab.update ((name, named_tthms), thms_tab);
   7.134 +    val thms_tab' = Symtab.update ((name, named_thms), thms_tab);
   7.135      val const_idx' =
   7.136        if overwrite then make_const_idx thms_tab'
   7.137 -      else foldl add_const_idx (const_idx, named_tthms);
   7.138 +      else foldl add_const_idx (const_idx, named_thms);
   7.139    in
   7.140      r := {space = space', thms_tab = thms_tab', const_idx = const_idx'};
   7.141 -    named_tthms
   7.142 +    named_thms
   7.143    end;
   7.144  
   7.145  
   7.146 -(* add_tthms(s) *)
   7.147 +(* add_thms(s) *)
   7.148  
   7.149 -fun add_tthmx app_name app_att ((bname, tthmx), atts) thy =
   7.150 +fun add_thmx app_name app_att ((bname, thmx), atts) thy =
   7.151    let
   7.152 -    val (thy', tthmx') = app_att ((thy, tthmx), atts);
   7.153 -    val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx');
   7.154 -  in (thy', tthms'') end;
   7.155 +    val (thy', thmx') = app_att ((thy, thmx), atts);
   7.156 +    val thms'' = enter_thmx (Theory.sign_of thy') app_name (bname, thmx');
   7.157 +  in (thy', thms'') end;
   7.158  
   7.159 -fun add_tthmxs name app = Library.apply o map (fst oo add_tthmx name app);
   7.160 +fun add_thmxs name app = Library.apply o map (fst oo add_thmx name app);
   7.161  
   7.162 -val add_tthms = add_tthmxs name_single Attribute.apply;
   7.163 -val add_tthmss = add_tthmxs name_multi Attribute.applys;
   7.164 +val add_thms = add_thmxs name_single Thm.apply_attributes;
   7.165 +val add_thmss = add_thmxs name_multi Thm.applys_attributes;
   7.166  
   7.167  
   7.168 -(* have_tthmss *)
   7.169 +(* have_thmss *)
   7.170  
   7.171 -fun have_tthmss bname more_atts ths_atts thy =
   7.172 +fun have_thmss bname more_atts ths_atts thy =
   7.173    let
   7.174 -    fun app (x, (ths, atts)) = Attribute.applys ((x, ths), atts);
   7.175 -    val (thy', tthmss') =
   7.176 +    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
   7.177 +    val (thy', thmss') =
   7.178        foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts);
   7.179 -    val tthms'' = enter_tthmx (Theory.sign_of thy') name_multi (bname, flat tthmss');
   7.180 -  in (thy, tthms'') end;
   7.181 +    val thms'' = enter_thmx (Theory.sign_of thy') name_multi (bname, flat thmss');
   7.182 +  in (thy, thms'') end;
   7.183  
   7.184  
   7.185 -(* store_tthm *)
   7.186 +(* store_thm *)
   7.187  
   7.188 -fun store_tthm th_atts thy =
   7.189 -  let val (thy', [th']) = add_tthmx name_single Attribute.apply th_atts thy
   7.190 +fun store_thm th_atts thy =
   7.191 +  let val (thy', [th']) = add_thmx name_single Thm.apply_attributes th_atts thy
   7.192    in (thy', th') end;
   7.193  
   7.194  
   7.195  (* smart_store_thm *)
   7.196  
   7.197  fun smart_store_thm (name, thm) =
   7.198 -  let val [(thm', _)] = enter_tthmx (Thm.sign_of_thm thm) name_single (name, Attribute.tthm_of thm)
   7.199 -  in thm' end;
   7.200 +  hd (enter_thmx (Thm.sign_of_thm thm) name_single (name, thm));
   7.201  
   7.202  
   7.203  (* store axioms as theorems *)
   7.204 @@ -299,8 +290,8 @@
   7.205      let
   7.206        val named_axs = app_name name axs;
   7.207        val thy' = add named_axs thy;
   7.208 -      val tthms = map (Attribute.tthm_of o Thm.get_axiom thy' o fst) named_axs;
   7.209 -    in add_tthmss [((name, tthms), atts)] thy' end;
   7.210 +      val thms = map (Thm.get_axiom thy' o fst) named_axs;
   7.211 +    in add_thmss [((name, thms), atts)] thy' end;
   7.212  
   7.213    fun add_axs app_name add = Library.apply o map (add_ax app_name add);
   7.214  in
   7.215 @@ -441,7 +432,7 @@
   7.216    |> Theory.add_modesyntax ("", false)
   7.217      [("Goal", "prop => prop", Mixfix ("_", [0], 0))]
   7.218    |> local_path
   7.219 -  |> (add_defs o map Attribute.none)
   7.220 +  |> (add_defs o map Thm.no_attributes)
   7.221     [("flexpair_def", "(t =?= u) == (t == u::'a::{})"),
   7.222      ("Goal_def", "GOAL (PROP A) == PROP A")]
   7.223    |> end_theory;