rudimentary class target implementation
authorhaftmann
Thu May 24 08:37:39 2007 +0200 (2007-05-24)
changeset 23087ad7244663431
parent 23086 12320f6e2523
child 23088 a3f11e0ae90f
rudimentary class target implementation
src/HOL/Finite_Set.thy
src/HOL/Lattices.thy
src/HOL/Orderings.thy
src/Pure/Isar/theory_target.ML
src/Pure/Tools/class_package.ML
     1.1 --- a/src/HOL/Finite_Set.thy	Thu May 24 08:37:37 2007 +0200
     1.2 +++ b/src/HOL/Finite_Set.thy	Thu May 24 08:37:39 2007 +0200
     1.3 @@ -2602,7 +2602,7 @@
     1.4    fix A :: "'a set"
     1.5    show "Linorder.Min (op \<le>) A = Min A"
     1.6    by (simp add: Min_def Linorder.Min_def [OF Linorder.intro, OF linorder_axioms]
     1.7 -    linorder_class_min)
     1.8 +    ord_class.min)
     1.9  qed
    1.10  
    1.11  lemma Linorder_Max:
    1.12 @@ -2611,16 +2611,16 @@
    1.13    fix A :: "'a set"
    1.14    show "Linorder.Max (op \<le>) A = Max A"
    1.15    by (simp add: Max_def Linorder.Max_def [OF Linorder.intro, OF linorder_axioms]
    1.16 -    linorder_class_max)
    1.17 +    ord_class.max)
    1.18  qed
    1.19  
    1.20 -interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
    1.21 +interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]:
    1.22    Linorder_ab_semigroup_add ["op \<le> \<Colon> 'a\<Colon>{linorder, pordered_ab_semigroup_add} \<Rightarrow> 'a \<Rightarrow> bool" "op <" "op +"]
    1.23    by (rule Linorder_ab_semigroup_add.intro,
    1.24      rule Linorder.intro, rule linorder_axioms, rule pordered_ab_semigroup_add_axioms)
    1.25  hide const Min Max
    1.26  
    1.27 -interpretation [unfolded linorder_class_min linorder_class_max Linorder_Min Linorder_Max]:
    1.28 +interpretation [folded ord_class.min ord_class.max, unfolded Linorder_Min Linorder_Max]:
    1.29    Linorder ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <"]
    1.30    by (rule Linorder.intro, rule linorder_axioms)
    1.31  declare Min_singleton [simp]
     2.1 --- a/src/HOL/Lattices.thy	Thu May 24 08:37:37 2007 +0200
     2.2 +++ b/src/HOL/Lattices.thy	Thu May 24 08:37:39 2007 +0200
     2.3 @@ -295,7 +295,7 @@
     2.4  
     2.5  interpretation min_max:
     2.6    distrib_lattice ["op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool" "op <" min max]
     2.7 -  by (rule distrib_lattice_min_max [unfolded linorder_class_min linorder_class_max])
     2.8 +  by (rule distrib_lattice_min_max [folded ord_class.min ord_class.max])
     2.9  
    2.10  lemma inf_min: "inf = (min \<Colon> 'a\<Colon>{lower_semilattice, linorder} \<Rightarrow> 'a \<Rightarrow> 'a)"
    2.11    by (rule ext)+ auto
     3.1 --- a/src/HOL/Orderings.thy	Thu May 24 08:37:37 2007 +0200
     3.2 +++ b/src/HOL/Orderings.thy	Thu May 24 08:37:39 2007 +0200
     3.3 @@ -81,26 +81,8 @@
     3.4  notation (input)
     3.5    greater_eq  (infix "\<ge>" 50)
     3.6  
     3.7 -hide const min max
     3.8 -
     3.9 -definition
    3.10 -  min :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    3.11 -  "min a b = (if a \<le> b then a else b)"
    3.12 -
    3.13 -definition
    3.14 -  max :: "'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> 'a" where
    3.15 -  "max a b = (if a \<le> b then b else a)"
    3.16 -
    3.17 -declare min_def[code unfold, code inline del]
    3.18 -        max_def[code unfold, code inline del]
    3.19 -
    3.20 -lemma linorder_class_min:
    3.21 -  "ord.min (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = min"
    3.22 -  by rule+ (simp add: min_def ord_class.min_def)
    3.23 -
    3.24 -lemma linorder_class_max:
    3.25 -  "ord.max (op \<le> \<Colon> 'a\<Colon>ord \<Rightarrow> 'a \<Rightarrow> bool) = max"
    3.26 -  by rule+ (simp add: max_def ord_class.max_def)
    3.27 +lemmas min_def [code func, code unfold, code inline del] = min_def [folded ord_class.min]
    3.28 +lemmas max_def [code func, code unfold, code inline del] = max_def [folded ord_class.max]
    3.29  
    3.30  
    3.31  subsection {* Partial orders *}
    3.32 @@ -351,14 +333,14 @@
    3.33  lemmas leD = linorder_class.leD
    3.34  lemmas not_leE = linorder_class.not_leE
    3.35  
    3.36 -lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [unfolded linorder_class_min]
    3.37 -lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [unfolded linorder_class_max]
    3.38 -lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [unfolded linorder_class_min]
    3.39 -lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [unfolded linorder_class_max]
    3.40 -lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [unfolded linorder_class_min]
    3.41 -lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [unfolded linorder_class_max]
    3.42 -lemmas split_min = linorder_class.split_min [unfolded linorder_class_min]
    3.43 -lemmas split_max = linorder_class.split_max [unfolded linorder_class_max]
    3.44 +lemmas min_le_iff_disj = linorder_class.min_le_iff_disj [folded ord_class.min]
    3.45 +lemmas le_max_iff_disj = linorder_class.le_max_iff_disj [folded ord_class.max]
    3.46 +lemmas min_less_iff_disj = linorder_class.min_less_iff_disj [folded ord_class.min]
    3.47 +lemmas less_max_iff_disj = linorder_class.less_max_iff_disj [folded ord_class.max]
    3.48 +lemmas min_less_iff_conj [simp] = linorder_class.min_less_iff_conj [folded ord_class.min]
    3.49 +lemmas max_less_iff_conj [simp] = linorder_class.max_less_iff_conj [folded ord_class.max]
    3.50 +lemmas split_min = linorder_class.split_min [folded ord_class.min]
    3.51 +lemmas split_max = linorder_class.split_max [folded ord_class.max]
    3.52  
    3.53  
    3.54  subsection {* Reasoning tools setup *}
     4.1 --- a/src/Pure/Isar/theory_target.ML	Thu May 24 08:37:37 2007 +0200
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Thu May 24 08:37:39 2007 +0200
     4.3 @@ -55,8 +55,8 @@
     4.4  
     4.5  fun internal_abbrev prmode ((c, mx), t) =
     4.6    (* FIXME really permissive *)
     4.7 -  LocalTheory.term_syntax (perhaps o try o ProofContext.target_abbrev prmode ((c, mx), t)) #>
     4.8 -  ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
     4.9 +  LocalTheory.term_syntax (perhaps o try o ProofContext.target_abbrev prmode ((c, mx), t))
    4.10 +  #> ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
    4.11  
    4.12  fun consts is_loc some_class depends decls lthy =
    4.13    let
    4.14 @@ -70,12 +70,19 @@
    4.15          val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
    4.16        in (((c, mx2), t), thy') end;
    4.17  
    4.18 -    val (abbrs, lthy') = lthy |> LocalTheory.theory_result (fold_map const decls);
    4.19 +    fun const_class (SOME class) ((c, _), mx) (_, t) =
    4.20 +          ClassPackage.add_const_in_class class ((c, t), mx)
    4.21 +      | const_class NONE _ _ = I;
    4.22 +
    4.23 +    val (abbrs, lthy') = lthy
    4.24 +      |> LocalTheory.theory_result (fold_map const decls)
    4.25      val defs = map (apsnd (pair ("", []))) abbrs;
    4.26    in
    4.27      lthy'
    4.28      |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
    4.29 -    |> LocalDefs.add_defs defs |>> map (apsnd snd)
    4.30 +    |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
    4.31 +    |> LocalDefs.add_defs defs
    4.32 +    |>> map (apsnd snd)
    4.33    end;
    4.34  
    4.35  
    4.36 @@ -85,7 +92,7 @@
    4.37    #1 (ProofContext.inferred_fixes ctxt)
    4.38    |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts []));
    4.39  
    4.40 -fun abbrev is_loc some_class  prmode ((raw_c, mx), raw_t) lthy =
    4.41 +fun abbrev is_loc some_class prmode ((raw_c, mx), raw_t) lthy =
    4.42    let
    4.43      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    4.44      val target = LocalTheory.target_of lthy;
    4.45 @@ -127,15 +134,16 @@
    4.46  
    4.47  in
    4.48  
    4.49 -fun defs loc some_class kind args lthy0 =
    4.50 +fun defs loc kind args lthy0 =
    4.51    let
    4.52      fun def ((c, mx), ((name, atts), rhs)) lthy1 =
    4.53        let
    4.54          val (rhs', rhs_conv) = expand_term lthy0 rhs;
    4.55          val xs = Variable.add_fixed (LocalTheory.target_of lthy0) rhs' [];
    4.56 +        val T = Term.fastype_of rhs;
    4.57  
    4.58          val ([(lhs, lhs_def)], lthy2) = lthy1
    4.59 -          |> LocalTheory.consts (member (op =) xs) [((c, Term.fastype_of rhs), mx)];
    4.60 +          |> LocalTheory.consts (member (op =) xs) [((c, T), mx)];
    4.61          val lhs' = #2 (Logic.dest_equals (Thm.prop_of lhs_def));
    4.62  
    4.63          val name' = Thm.def_name_optional c name;
    4.64 @@ -145,14 +153,7 @@
    4.65            [(*c == loc.c xs*) lhs_def,
    4.66             (*lhs' == rhs'*)  def,
    4.67             (*rhs' == rhs*)   Thm.symmetric rhs_conv];
    4.68 -        val lthy4 = case some_class
    4.69 -         of SOME class => 
    4.70 -              lthy3
    4.71 -              |> LocalTheory.raw_theory
    4.72 -                (ClassPackage.add_def_in_class lthy3 class
    4.73 -                  ((c, mx), ((name, atts), (rhs, eq))))
    4.74 -          | _ => lthy3;
    4.75 -      in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
    4.76 +      in ((lhs, ((name', atts), [([eq], [])])), lthy3) end;
    4.77  
    4.78      val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
    4.79      val (res, lthy'') = lthy' |> LocalTheory.notes kind facts;
    4.80 @@ -320,7 +321,7 @@
    4.81        consts = consts is_loc some_class,
    4.82        axioms = axioms,
    4.83        abbrev = abbrev is_loc some_class,
    4.84 -      defs = defs loc some_class,
    4.85 +      defs = defs loc,
    4.86        notes = notes loc,
    4.87        type_syntax = type_syntax loc,
    4.88        term_syntax = term_syntax loc,
     5.1 --- a/src/Pure/Tools/class_package.ML	Thu May 24 08:37:37 2007 +0200
     5.2 +++ b/src/Pure/Tools/class_package.ML	Thu May 24 08:37:39 2007 +0200
     5.3 @@ -29,11 +29,9 @@
     5.4    val instance_sort_cmd: string * string -> theory -> Proof.state
     5.5    val prove_instance_sort: tactic -> class * sort -> theory -> theory
     5.6  
     5.7 -  (* experimental class target *)
     5.8    val class_of_locale: theory -> string -> class option
     5.9 -  val add_def_in_class: local_theory -> string
    5.10 -    -> (string * Syntax.mixfix) * ((string * Attrib.src list) * (term * thm)) -> theory -> theory
    5.11 -  val CLASS_TARGET: bool ref
    5.12 +  val add_const_in_class: string -> (string * term) * Syntax.mixfix
    5.13 +    -> theory -> theory
    5.14  
    5.15    val print_classes: theory -> unit
    5.16    val intro_classes_tac: thm list -> tactic
    5.17 @@ -88,7 +86,7 @@
    5.18    gen_instance (single oo (Logic.mk_classrel oo AxClass.cert_classrel))
    5.19      AxClass.add_classrel I o single;
    5.20  
    5.21 -end; (* local *)
    5.22 +end; (*local*)
    5.23  
    5.24  
    5.25  (* introducing axclasses with implicit parameter handling *)
    5.26 @@ -222,7 +220,7 @@
    5.27  val instance_arity = instance_arity' axclass_instance_arity;
    5.28  val prove_instance_arity = instance_arity' o tactic_proof;
    5.29  
    5.30 -end; (* local *)
    5.31 +end; (*local*)
    5.32  
    5.33  
    5.34  
    5.35 @@ -234,10 +232,8 @@
    5.36    locale: string,
    5.37    consts: (string * string) list
    5.38      (*locale parameter ~> toplevel theory constant*),
    5.39 +  v: string option,
    5.40    intro: thm,
    5.41 -  witness: Element.witness list,
    5.42 -  primdefs: thm list,
    5.43 -    (*for experimental class target*)
    5.44    propnames: string list
    5.45      (*for ad-hoc instance_in*)
    5.46  };
    5.47 @@ -282,7 +278,7 @@
    5.48  fun these_intros thy =
    5.49    Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_classdata) data))
    5.50      ((fst o ClassData.get) thy) [];
    5.51 -val the_witness = #witness oo the_class_data;
    5.52 +
    5.53  val the_propnames = #propnames oo the_class_data;
    5.54  
    5.55  fun print_classes thy =
    5.56 @@ -320,44 +316,21 @@
    5.57  
    5.58  (* updaters *)
    5.59  
    5.60 -fun add_class_data ((class, superclasses), (locale, consts, intro, witness, propnames)) =
    5.61 +fun add_class_data ((class, superclasses), (locale, consts, v, intro, propnames)) =
    5.62    ClassData.map (fn (gr, tab) => (
    5.63      gr
    5.64      |> Graph.new_node (class, ClassData {
    5.65        locale = locale,
    5.66        consts = consts,
    5.67 +      v = v,
    5.68        intro = intro,
    5.69 -      witness = witness,
    5.70 -      propnames = propnames,
    5.71 -      primdefs = []})
    5.72 +      propnames = propnames}
    5.73 +    )
    5.74      |> fold (curry Graph.add_edge class) superclasses,
    5.75      tab
    5.76      |> Symtab.update (locale, class)
    5.77    ));
    5.78  
    5.79 -fun add_primdef (class, thm) thy =
    5.80 -  (ClassData.map o apfst o Graph.map_node class)
    5.81 -    (fn ClassData { locale, consts, intro, witness, propnames, primdefs } =>
    5.82 -      ClassData { locale = locale, consts = consts, intro = intro,
    5.83 -        witness = witness, propnames = propnames, primdefs = thm :: primdefs });
    5.84 -
    5.85 -
    5.86 -(* exporting terms and theorems to global toplevel *)
    5.87 -
    5.88 -fun globalize thy classes =
    5.89 -  let
    5.90 -    val consts = param_map thy classes;
    5.91 -    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) classes;
    5.92 -    val subst_typ = Term.map_type_tfree (fn var as (v, sort) =>
    5.93 -      if v = AxClass.param_tyvarname then TFree (v, constrain_sort sort) else TFree var)
    5.94 -    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
    5.95 -         of SOME (c, _) => Const (c, ty)
    5.96 -          | NONE => t)
    5.97 -      | subst_aterm t = t;
    5.98 -  in (subst_typ, map_types subst_typ #> Term.map_aterms subst_aterm) end;
    5.99 -
   5.100 -val global_term = snd oo globalize
   5.101 -
   5.102  
   5.103  (* tactics and methods *)
   5.104  
   5.105 @@ -524,12 +497,15 @@
   5.106      fun extract_params thy name_locale =
   5.107        let
   5.108          val params = Locale.parameters_of thy name_locale;
   5.109 +        val v = case (maps typ_tfrees o map (snd o fst)) params
   5.110 +         of (v, _) :: _ => SOME v
   5.111 +          | _ => NONE;
   5.112        in
   5.113 -        (map (fst o fst) params, params
   5.114 +        (v, (map (fst o fst) params, params
   5.115          |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   5.116          |> (map o apsnd) (fork_mixfix true NONE #> fst)
   5.117          |> chop (length supconsts)
   5.118 -        |> snd)
   5.119 +        |> snd))
   5.120        end;
   5.121      fun extract_assumes name_locale params thy cs =
   5.122        let
   5.123 @@ -554,7 +530,6 @@
   5.124        Symtab.empty
   5.125        |> fold2 (fn v => fn (c, ty) => Symtab.update (v, Const
   5.126             (c, Term.map_type_tfree (fn (v, _) => TFree (v, [class])) ty))) param_names cs;
   5.127 -    fun make_witness t thm = Element.make_witness t (Goal.protect thm);
   5.128      fun note_intro name_axclass class_intro =
   5.129        PureThy.note_thmss_qualified "" ((Logic.const_of_class o NameSpace.base) name_axclass)
   5.130          [(("intro", []), [([class_intro], [])])]
   5.131 @@ -564,15 +539,15 @@
   5.132      |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
   5.133      |-> (fn name_locale => ProofContext.theory_result (
   5.134        `(fn thy => extract_params thy name_locale)
   5.135 -      #-> (fn (param_names, params) =>
   5.136 +      #-> (fn (v, (param_names, params)) =>
   5.137          axclass_params (bname, supsort) params (extract_assumes name_locale params) other_consts
   5.138        #-> (fn (name_axclass, ((_, (ax_terms, ax_axioms)), consts)) =>
   5.139          `(fn thy => class_intro thy name_locale name_axclass sups)
   5.140        ##>> `(fn thy => extract_axiom_names thy name_locale)
   5.141        #-> (fn (class_intro, axiom_names) =>
   5.142          add_class_data ((name_axclass, sups),
   5.143 -          (name_locale, map (fst o fst) params ~~ map fst consts,
   5.144 -            class_intro, map2 make_witness ax_terms ax_axioms, axiom_names))
   5.145 +          (name_locale, map (fst o fst) params ~~ map fst consts, v,
   5.146 +            class_intro, axiom_names))
   5.147        #> note_intro name_axclass class_intro
   5.148        #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
   5.149            ((false, Logic.const_of_class bname), []) (Locale.Locale name_locale)
   5.150 @@ -615,69 +590,48 @@
   5.151  val instance_class_cmd = gen_instance_class Sign.read_class;
   5.152  val instance_class = gen_instance_class Sign.certify_class;
   5.153  
   5.154 -end; (* local *)
   5.155 +end; (*local*)
   5.156  
   5.157  
   5.158 -(** experimental class target **)
   5.159 +(** class target **)
   5.160  
   5.161 -fun print_witness wit =
   5.162 +fun export_fixes thy class =
   5.163    let
   5.164 -    val (t, thm) = Element.dest_witness wit;
   5.165 -    val prop = Thm.prop_of thm;
   5.166 -    fun string_of_tfree (v, sort) = v ^ "::" ^ Display.raw_string_of_sort sort;
   5.167 -    fun string_of_tvar (v, sort) = Library.string_of_indexname v ^ "::" ^ Display.raw_string_of_sort sort;
   5.168 -    fun print_term t =
   5.169 -      let
   5.170 -        val term = Display.raw_string_of_term t;
   5.171 -        val tfrees = map string_of_tfree (Term.add_tfrees t []);
   5.172 -        val tvars = map string_of_tvar (Term.add_tvars t []);
   5.173 -      in term :: tfrees @ tvars end;
   5.174 -  in (map warning (print_term t); map warning (print_term prop)) end;
   5.175 +    val v = (#v o the_class_data thy) class;
   5.176 +    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   5.177 +    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   5.178 +      if SOME w = v then TFree (w, constrain_sort sort) else TFree var);
   5.179 +    val consts = param_map thy [class];
   5.180 +    fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   5.181 +         of SOME (c, _) => Const (c, ty)
   5.182 +          | NONE => t)
   5.183 +      | subst_aterm t = t;
   5.184 +  in map_types subst_typ #> Term.map_aterms subst_aterm end;
   5.185  
   5.186 -val CLASS_TARGET = ref true;
   5.187 -
   5.188 -fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
   5.189 +fun add_const_in_class class ((c, rhs), syn) thy =
   5.190    let
   5.191      val prfx = (Logic.const_of_class o NameSpace.base) class;
   5.192 -    val rhs' = global_term thy [class] rhs;
   5.193 -    val (syn', _) = fork_mixfix true NONE syn;
   5.194 -    val ty = Term.fastype_of rhs';
   5.195 -    fun mk_name thy c =
   5.196 +    fun mk_name inject c =
   5.197        let
   5.198          val n1 = Sign.full_name thy c;
   5.199          val n2 = NameSpace.qualifier n1;
   5.200          val n3 = NameSpace.base n1;
   5.201 -      in NameSpace.implode [n2, prfx, n3] end;
   5.202 -    fun add_const (c, ty, syn) =
   5.203 -      Sign.add_consts_authentic [(c, ty, syn)]
   5.204 -      #> pair (mk_name thy c, ty);
   5.205 -    fun add_def ((name, atts), prop) thy =
   5.206 -      thy
   5.207 -      |> PureThy.add_defs_i false [((name, prop), map (Attrib.attribute thy) atts)]
   5.208 -      |>> the_single;
   5.209 -    (*val _ = warning "------ DEF ------";
   5.210 -    val _ = warning c;
   5.211 -    val _ = warning name;
   5.212 -    val _ = (warning o Sign.string_of_term thy) rhs';
   5.213 -    val eq' = Morphism.thm (LocalTheory.target_morphism lthy) eq;
   5.214 -    val _ = (warning o string_of_thm) eq;
   5.215 -    val _ = (warning o string_of_thm) eq';
   5.216 -    val witness = the_witness thy class;
   5.217 -    val _ = warning "------ WIT ------";
   5.218 -    fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")"
   5.219 -    fun print_raw_wit (t, thm) = "(" ^ Display.raw_string_of_term t ^ ", " ^ (Display.raw_string_of_term o Thm.prop_of) thm ^ ")"
   5.220 -    val _ = (warning o cat_lines o map (print_wit o Element.dest_witness)) witness;
   5.221 -    val _ = map print_witness witness;
   5.222 -    val _ = (warning o string_of_thm) eq';
   5.223 -    val eq'' = Element.satisfy_thm witness eq';
   5.224 -    val _ = (warning o string_of_thm) eq'';*)
   5.225 +      in NameSpace.implode (n2 :: inject @ [n3]) end;
   5.226 +    val abbr' = mk_name [prfx, prfx] c;
   5.227 +    val rhs' = export_fixes thy class rhs;
   5.228 +    val ty' = Term.fastype_of rhs';
   5.229 +    val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));
   5.230 +    val (syn', _) = fork_mixfix true NONE syn;
   5.231    in
   5.232      thy
   5.233 -    (* |> Sign.add_path prfx
   5.234 -    |> add_const (c, ty, syn')
   5.235 -    |-> (fn c => add_def ((name, atts), Logic.mk_equals (Const c, rhs')))
   5.236 -    |-> (fn global_def_thm => tap (fn _ => (warning o string_of_thm) global_def_thm))
   5.237 -    |> Sign.restore_naming thy *)
   5.238 +    |> Sign.hide_consts_i true [abbr']
   5.239 +    |> Sign.add_path prfx
   5.240 +    |> Sign.add_consts_authentic [(c, ty', syn')]
   5.241 +    |> Sign.parent_path
   5.242 +    |> Sign.sticky_prefix prfx
   5.243 +    |> PureThy.add_defs_i false [(def, [])]
   5.244 +    |> snd
   5.245 +    |> Sign.restore_naming thy
   5.246    end;
   5.247  
   5.248  end;