fixed wrong syntax treatment in class target
authorhaftmann
Thu Sep 20 16:37:29 2007 +0200 (2007-09-20)
changeset 24657185502d54c3d
parent 24656 67f6bf194ca6
child 24658 49adbdcc52e2
fixed wrong syntax treatment in class target
src/HOL/List.thy
src/HOL/ex/Classpackage.thy
src/Pure/Isar/class.ML
src/Pure/Isar/theory_target.ML
     1.1 --- a/src/HOL/List.thy	Thu Sep 20 16:37:28 2007 +0200
     1.2 +++ b/src/HOL/List.thy	Thu Sep 20 16:37:29 2007 +0200
     1.3 @@ -215,18 +215,23 @@
     1.4  text{* The following simple sort functions are intended for proofs,
     1.5  not for efficient implementations. *}
     1.6  
     1.7 -fun (in linorder) sorted :: "'a list \<Rightarrow> bool" where
     1.8 -"sorted [] \<longleftrightarrow> True" |
     1.9 -"sorted [x] \<longleftrightarrow> True" |
    1.10 -"sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
    1.11 -
    1.12 -fun (in linorder) insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.13 -"insort x [] = [x]" |
    1.14 -"insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
    1.15 -
    1.16 -fun (in linorder) sort :: "'a list \<Rightarrow> 'a list" where
    1.17 -"sort [] = []" |
    1.18 -"sort (x#xs) = insort x (sort xs)"
    1.19 +context linorder
    1.20 +begin
    1.21 +
    1.22 +fun  sorted :: "'a list \<Rightarrow> bool" where
    1.23 +  "sorted [] \<longleftrightarrow> True" |
    1.24 +  "sorted [x] \<longleftrightarrow> True" |
    1.25 +  "sorted (x#y#zs) \<longleftrightarrow> x \<^loc><= y \<and> sorted (y#zs)"
    1.26 +
    1.27 +fun insort :: "'a \<Rightarrow> 'a list \<Rightarrow> 'a list" where
    1.28 +  "insort x [] = [x]" |
    1.29 +  "insort x (y#ys) = (if x \<^loc><= y then (x#y#ys) else y#(insort x ys))"
    1.30 +
    1.31 +fun sort :: "'a list \<Rightarrow> 'a list" where
    1.32 +  "sort [] = []" |
    1.33 +  "sort (x#xs) = insort x (sort xs)"
    1.34 +
    1.35 +end
    1.36  
    1.37  
    1.38  subsubsection {* List comprehension *}
     2.1 --- a/src/HOL/ex/Classpackage.thy	Thu Sep 20 16:37:28 2007 +0200
     2.2 +++ b/src/HOL/ex/Classpackage.thy	Thu Sep 20 16:37:29 2007 +0200
     2.3 @@ -81,8 +81,6 @@
     2.4    units :: "'a set" where
     2.5    "units = {y. \<exists>x. x \<^loc>\<otimes> y = \<^loc>\<one> \<and> y \<^loc>\<otimes> x = \<^loc>\<one>}"
     2.6  
     2.7 -end context monoid begin
     2.8 -
     2.9  lemma inv_obtain:
    2.10    assumes "x \<in> units"
    2.11    obtains y where "y \<^loc>\<otimes> x = \<^loc>\<one>" and "x \<^loc>\<otimes> y = \<^loc>\<one>"
    2.12 @@ -120,8 +118,6 @@
    2.13    "npow 0 x = \<^loc>\<one>"
    2.14    | "npow (Suc n) x = x \<^loc>\<otimes> npow n x"
    2.15  
    2.16 -end context monoid begin
    2.17 -
    2.18  abbreviation
    2.19    npow_syn :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infix "\<^loc>\<up>" 75) where
    2.20    "x \<^loc>\<up> n \<equiv> npow n x"
     3.1 --- a/src/Pure/Isar/class.ML	Thu Sep 20 16:37:28 2007 +0200
     3.2 +++ b/src/Pure/Isar/class.ML	Thu Sep 20 16:37:29 2007 +0200
     3.3 @@ -44,6 +44,14 @@
     3.4    val inst_const: theory -> string * string -> string
     3.5    val param_const: theory -> string -> (string * string) option
     3.6    val params_of_sort: theory -> sort -> (string * (string * typ)) list
     3.7 +
     3.8 +  (*experimental*)
     3.9 +  val init_ref: (class -> Proof.context -> (theory -> theory) * Proof.context) ref
    3.10 +  val init: class -> Proof.context -> (theory -> theory) * Proof.context;
    3.11 +  val init_default: class -> Proof.context -> (theory -> theory) * Proof.context;
    3.12 +  val remove_constraints: class -> theory -> (string * typ) list * theory
    3.13 +  val class_term_check: theory -> class -> term list -> Proof.context -> term list * Proof.context
    3.14 +  val local_param: theory -> class -> string -> (term * (class * int)) option
    3.15  end;
    3.16  
    3.17  structure Class : CLASS =
    3.18 @@ -91,6 +99,15 @@
    3.19        | NONE => thm;
    3.20    in strip end;
    3.21  
    3.22 +fun get_remove_contraint c thy =
    3.23 +  let
    3.24 +    val ty = Sign.the_const_constraint thy c;
    3.25 +  in
    3.26 +    thy
    3.27 +    |> Sign.add_const_constraint_i (c, NONE)
    3.28 +    |> pair (c, Logic.unvarifyT ty)
    3.29 +  end;
    3.30 +
    3.31  
    3.32  (** axclass command **)
    3.33  
    3.34 @@ -277,14 +294,6 @@
    3.35        in fold_map read defs cs end;
    3.36      val (defs, other_cs) = read_defs raw_defs cs
    3.37        (fold Sign.primitive_arity arities (Theory.copy theory));
    3.38 -    fun get_remove_contraint c thy =
    3.39 -      let
    3.40 -        val ty = Sign.the_const_constraint thy c;
    3.41 -      in
    3.42 -        thy
    3.43 -        |> Sign.add_const_constraint_i (c, NONE)
    3.44 -        |> pair (c, Logic.unvarifyT ty)
    3.45 -      end;
    3.46      fun after_qed' cs defs =
    3.47        fold Sign.add_const_constraint_i (map (apsnd SOME) cs)
    3.48        #> after_qed defs;
    3.49 @@ -320,30 +329,45 @@
    3.50  datatype class_data = ClassData of {
    3.51    locale: string,
    3.52    consts: (string * string) list
    3.53 -    (*locale parameter ~> toplevel theory constant*),
    3.54 -  v: string option,
    3.55 +    (*locale parameter ~> theory constant name*),
    3.56 +  v: string,
    3.57    inst: typ Symtab.table * term Symtab.table
    3.58      (*canonical interpretation*),
    3.59 -  intro: thm
    3.60 -} * thm list (*derived defs*);
    3.61 +  intro: thm,
    3.62 +  defs: thm list,
    3.63 +  localized: (string * (term * (class * int))) list
    3.64 +    (*theory constant name ~> (locale parameter, (class, instantiaton index of class typ))*)
    3.65 +};
    3.66  
    3.67 -fun rep_classdata (ClassData c) = c;
    3.68 +fun rep_class_data (ClassData d) = d;
    3.69 +fun mk_class_data ((locale, consts, v, inst, intro), (defs, localized)) =
    3.70 +  ClassData { locale = locale, consts = consts, v = v, inst = inst, intro = intro,
    3.71 +    defs = defs, localized = localized };
    3.72 +fun map_class_data f (ClassData { locale, consts, v, inst, intro, defs, localized }) =
    3.73 +  mk_class_data (f ((locale, consts, v, inst, intro), (defs, localized)))
    3.74 +fun merge_class_data _ (ClassData { locale = locale, consts = consts, v = v, inst = inst,
    3.75 +    intro = intro, defs = defs1, localized = localized1 },
    3.76 +  ClassData { locale = _, consts = _, v = _, inst = _, intro = _,
    3.77 +    defs = defs2, localized = localized2 }) =
    3.78 +  mk_class_data ((locale, consts, v, inst, intro),
    3.79 +    (Thm.merge_thms (defs1, defs2), AList.merge (op =) (K true) (localized1, localized2)));
    3.80  
    3.81  fun merge_pair f1 f2 ((x1, y1), (x2, y2)) = (f1 (x1, x2), f2 (y1, y2));
    3.82  
    3.83  structure ClassData = TheoryDataFun
    3.84  (
    3.85 -  type T = class_data Graph.T * class Symtab.table (*locale name ~> class name*);
    3.86 +  type T = class_data Graph.T * class Symtab.table
    3.87 +    (*locale name ~> class name*);
    3.88    val empty = (Graph.empty, Symtab.empty);
    3.89    val copy = I;
    3.90    val extend = I;
    3.91 -  fun merge _ = merge_pair (Graph.merge (K true)) (Symtab.merge (K true));
    3.92 +  fun merge _ = merge_pair (Graph.join merge_class_data) (Symtab.merge (K true));
    3.93  );
    3.94  
    3.95  
    3.96  (* queries *)
    3.97  
    3.98 -val lookup_class_data = Option.map rep_classdata oo try o Graph.get_node
    3.99 +val lookup_class_data = Option.map rep_class_data oo try o Graph.get_node
   3.100    o fst o ClassData.get;
   3.101  fun class_of_locale thy = Symtab.lookup ((snd o ClassData.get) thy);
   3.102  
   3.103 @@ -358,18 +382,23 @@
   3.104      fun params class =
   3.105        let
   3.106          val const_typs = (#params o AxClass.get_definition thy) class;
   3.107 -        val const_names = (#consts o fst o the_class_data thy) class;
   3.108 +        val const_names = (#consts o the_class_data thy) class;
   3.109        in
   3.110          (map o apsnd) (fn c => (c, (the o AList.lookup (op =) const_typs) c)) const_names
   3.111        end;
   3.112    in maps params o ancestry thy end;
   3.113  
   3.114 -fun these_defs thy = maps (these o Option.map snd o lookup_class_data thy) o ancestry thy;
   3.115 +fun these_defs thy = maps (these o Option.map #defs o lookup_class_data thy) o ancestry thy;
   3.116  
   3.117  fun these_intros thy =
   3.118 -  Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o fst o rep_classdata) data))
   3.119 +  Graph.fold (fn (_, (data, _)) => insert Thm.eq_thm ((#intro o rep_class_data) data))
   3.120      ((fst o ClassData.get) thy) [];
   3.121  
   3.122 +fun these_localized thy class =
   3.123 +  maps (#localized o the_class_data thy) (ancestry thy [class]);
   3.124 +
   3.125 +fun local_param thy = AList.lookup (op =) o these_localized thy;
   3.126 +
   3.127  fun print_classes thy =
   3.128    let
   3.129      val algebra = Sign.classes_of thy;
   3.130 @@ -389,7 +418,7 @@
   3.131        (SOME o Pretty.str) ("class " ^ class ^ ":"),
   3.132        (SOME o Pretty.block) [Pretty.str "supersort: ",
   3.133          (Sign.pretty_sort thy o Sign.certify_sort thy o Sign.super_classes thy) class],
   3.134 -      Option.map (Pretty.str o prefix "locale: " o #locale o fst) (lookup_class_data thy class),
   3.135 +      Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
   3.136        ((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
   3.137          o these o Option.map #params o try (AxClass.get_definition thy)) class,
   3.138        (SOME o Pretty.block o Pretty.breaks) [
   3.139 @@ -408,15 +437,16 @@
   3.140  fun add_class_data ((class, superclasses), (locale, consts, v, inst, intro)) =
   3.141    ClassData.map (fn (gr, tab) => (
   3.142      gr
   3.143 -    |> Graph.new_node (class, ClassData ({ locale = locale, consts = consts,
   3.144 -         v = v, inst = inst, intro = intro }, []))
   3.145 +    |> Graph.new_node (class, mk_class_data ((locale, (map o apfst) fst consts, v, inst, intro),
   3.146 +         ([], map (apsnd (rpair (class, 0) o Free) o swap) consts)))
   3.147      |> fold (curry Graph.add_edge class) superclasses,
   3.148      tab
   3.149      |> Symtab.update (locale, class)
   3.150    ));
   3.151  
   3.152 -fun add_class_const_thm (class, thm) = (ClassData.map o apfst o Graph.map_node class)
   3.153 -  (fn ClassData (data, thms) => ClassData (data, thm :: thms));
   3.154 +fun add_class_const_def (class, (entry, def)) =
   3.155 +  (ClassData.map o apfst o Graph.map_node class o map_class_data o apsnd)
   3.156 +    (fn (defs, localized) => (def :: defs, (apsnd o apsnd) (pair class) entry :: localized));
   3.157  
   3.158  
   3.159  (** rule calculation, tactics and methods **)
   3.160 @@ -452,7 +482,7 @@
   3.161  
   3.162  fun class_interpretation class facts defs thy =
   3.163    let
   3.164 -    val ({ locale, inst, ... }, _) = the_class_data thy class;
   3.165 +    val { locale, inst, ... } = the_class_data thy class;
   3.166      val tac = (ALLGOALS o ProofContext.fact_tac) facts;
   3.167      val prfx = Logic.const_of_class (NameSpace.base class);
   3.168    in
   3.169 @@ -464,7 +494,7 @@
   3.170    let
   3.171      fun mk_axioms class =
   3.172        let
   3.173 -        val ({ locale, inst = (_, insttab), ... }, _) = the_class_data thy class;
   3.174 +        val { locale, inst = (_, insttab), ... } = the_class_data thy class;
   3.175        in
   3.176          Locale.global_asms_of thy locale
   3.177          |> maps snd
   3.178 @@ -546,7 +576,7 @@
   3.179      val sups = filter (is_some o lookup_class_data thy) supclasses
   3.180        |> Sign.certify_sort thy;
   3.181      val supsort = Sign.certify_sort thy supclasses;
   3.182 -    val suplocales = map (Locale.Locale o #locale o fst o the_class_data thy) sups;
   3.183 +    val suplocales = map (Locale.Locale o #locale o the_class_data thy) sups;
   3.184      val supexpr = Locale.Merge (suplocales @ includes);
   3.185      val supparams = (map fst o Locale.parameters_of_expr thy)
   3.186        (Locale.Merge suplocales);
   3.187 @@ -563,10 +593,10 @@
   3.188        let
   3.189          val params = Locale.parameters_of thy name_locale;
   3.190          val v = case (maps typ_tfrees o map (snd o fst)) params
   3.191 -         of (v, _) :: _ => SOME v
   3.192 -          | _ => NONE;
   3.193 +         of (v, _) :: _ => v
   3.194 +          | [] => AxClass.param_tyvarname;
   3.195        in
   3.196 -        (v, (map (fst o fst) params, params
   3.197 +        (v, (map fst params, params
   3.198          |> (map o apfst o apsnd o Term.map_type_tfree) mk_tyvar
   3.199          |> (map o apsnd) (fork_mixfix true NONE #> fst)
   3.200          |> chop (length supconsts)
   3.201 @@ -578,7 +608,6 @@
   3.202          fun subst (Free (c, ty)) =
   3.203                Const ((fst o the o AList.lookup (op =) consts) c, ty)
   3.204            | subst t = t;
   3.205 -        val super_defs = these_defs thy sups;
   3.206          fun prep_asm ((name, atts), ts) =
   3.207            ((NameSpace.base name, map (Attrib.attribute thy) atts),
   3.208              (map o map_aterms) subst ts);
   3.209 @@ -595,15 +624,15 @@
   3.210      |> add_locale (SOME "") bname supexpr ((*elems_constrains @*) elems)
   3.211      |-> (fn name_locale => ProofContext.theory_result (
   3.212        `(fn thy => extract_params thy name_locale)
   3.213 -      #-> (fn (v, (param_names, params)) =>
   3.214 +      #-> (fn (v, (globals, params)) =>
   3.215          AxClass.define_class_params (bname, supsort) params
   3.216            (extract_assumes name_locale params) other_consts
   3.217        #-> (fn (name_axclass, (consts, axioms)) =>
   3.218          `(fn thy => class_intro thy name_locale name_axclass sups)
   3.219        #-> (fn class_intro =>
   3.220          add_class_data ((name_axclass, sups),
   3.221 -          (name_locale, map (fst o fst) params ~~ map fst consts, v,
   3.222 -            (mk_instT name_axclass, mk_inst name_axclass param_names
   3.223 +          (name_locale, map fst params ~~ map fst consts, v,
   3.224 +            (mk_instT name_axclass, mk_inst name_axclass (map fst globals)
   3.225                (map snd supconsts @ consts)), class_intro))
   3.226        #> note_intro name_axclass class_intro
   3.227        #> class_interpretation name_axclass axioms []
   3.228 @@ -619,52 +648,62 @@
   3.229  end; (*local*)
   3.230  
   3.231  
   3.232 +(* class target context *)
   3.233 +
   3.234 +fun remove_constraints class thy =
   3.235 +  thy |> fold_map (get_remove_contraint o fst) (these_localized thy class);
   3.236 +
   3.237 +
   3.238  (* definition in class target *)
   3.239  
   3.240  fun export_fixes thy class =
   3.241    let
   3.242 -    val v = (#v o fst o the_class_data thy) class;
   3.243 -    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   3.244 -    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   3.245 -      if SOME w = v then TFree (w, constrain_sort sort) else TFree var);
   3.246      val consts = params_of_sort thy [class];
   3.247      fun subst_aterm (t as Free (v, ty)) = (case AList.lookup (op =) consts v
   3.248           of SOME (c, _) => Const (c, ty)
   3.249            | NONE => t)
   3.250        | subst_aterm t = t;
   3.251 -  in map_types subst_typ #> Term.map_aterms subst_aterm end;
   3.252 +  in Term.map_aterms subst_aterm end;
   3.253  
   3.254  fun add_const_in_class class ((c, rhs), syn) thy =
   3.255    let
   3.256      val prfx = (Logic.const_of_class o NameSpace.base) class;
   3.257 -    fun mk_name inject c =
   3.258 +    fun mk_name c =
   3.259        let
   3.260          val n1 = Sign.full_name thy c;
   3.261          val n2 = NameSpace.qualifier n1;
   3.262          val n3 = NameSpace.base n1;
   3.263 -      in NameSpace.implode (n2 :: inject @ [n3]) end;
   3.264 -    val abbr' = mk_name [prfx, prfx] c;
   3.265 +      in NameSpace.implode [n2, prfx, n3] end;
   3.266 +    val v = (#v o the_class_data thy) class;
   3.267 +    val constrain_sort = curry (Sorts.inter_sort (Sign.classes_of thy)) [class];
   3.268 +    val subst_typ = Term.map_type_tfree (fn var as (w, sort) =>
   3.269 +      if w = v then TFree (w, constrain_sort sort) else TFree var);
   3.270      val rhs' = export_fixes thy class rhs;
   3.271      val ty' = Term.fastype_of rhs';
   3.272 -    val def = (c, Logic.mk_equals (Const (mk_name [prfx] c, ty'), rhs'));
   3.273 +    val ty'' = subst_typ ty';
   3.274 +    val c' = mk_name c;
   3.275 +    val def = (c, Logic.mk_equals (Const (c', ty'), rhs'));
   3.276      val (syn', _) = fork_mixfix true NONE syn;
   3.277 -    fun interpret def =
   3.278 +    fun interpret def thy =
   3.279        let
   3.280          val def' = symmetric def;
   3.281          val def_eq = Thm.prop_of def';
   3.282 +        val typargs = Sign.const_typargs thy (c', fastype_of rhs);
   3.283 +        val typidx = find_index (fn TFree (w, _) => v = w | _ => false) typargs;
   3.284        in
   3.285 -        class_interpretation class [def'] [def_eq]
   3.286 -        #> add_class_const_thm (class, def')
   3.287 +        thy
   3.288 +        |> class_interpretation class [def'] [def_eq]
   3.289 +        |> add_class_const_def (class, ((c', (rhs, typidx)), def'))
   3.290        end;
   3.291    in
   3.292      thy
   3.293 -    |> Sign.hide_consts_i true [abbr']
   3.294      |> Sign.add_path prfx
   3.295      |> Sign.add_consts_authentic [(c, ty', syn')]
   3.296      |> Sign.parent_path
   3.297      |> Sign.sticky_prefix prfx
   3.298      |> PureThy.add_defs_i false [(def, [])]
   3.299      |-> (fn [def] => interpret def)
   3.300 +    |> Sign.add_const_constraint_i (c', SOME ty'')
   3.301      |> Sign.restore_naming thy
   3.302    end;
   3.303  
   3.304 @@ -677,8 +716,8 @@
   3.305    let
   3.306      val class = prep_class theory raw_class;
   3.307      val superclass = prep_class theory raw_superclass;
   3.308 -    val loc_name = (#locale o fst o the_class_data theory) class;
   3.309 -    val loc_expr = (Locale.Locale o #locale o fst o the_class_data theory) superclass;
   3.310 +    val loc_name = (#locale o the_class_data theory) class;
   3.311 +    val loc_expr = (Locale.Locale o #locale o the_class_data theory) superclass;
   3.312      fun prove_classrel (class, superclass) thy =
   3.313        let
   3.314          val classes = (Graph.all_succs o #classes o Sorts.rep_algebra
   3.315 @@ -717,4 +756,52 @@
   3.316  
   3.317  end; (*local*)
   3.318  
   3.319 +(*experimental*)
   3.320 +fun class_term_check thy class =
   3.321 +  let
   3.322 +    val algebra = Sign.classes_of thy;
   3.323 +    val { v, ... } = the_class_data thy class;
   3.324 +    fun add_constrain_classtyp sort' (ty as TFree (v, _)) =
   3.325 +          AList.map_default (op =) (v, []) (curry (Sorts.inter_sort algebra) sort')
   3.326 +      | add_constrain_classtyp sort' (Type (tyco, tys)) = case Sorts.mg_domain algebra tyco sort'
   3.327 +         of sorts => fold2 add_constrain_classtyp sorts tys;
   3.328 +    fun class_arg c idx ty =
   3.329 +      let
   3.330 +        val typargs = Sign.const_typargs thy (c, ty);
   3.331 +        fun classtyp (t as TFree (w, _)) = if w = v then NONE else SOME t
   3.332 +          | classtyp t = SOME t;
   3.333 +      in classtyp (nth typargs idx) end;
   3.334 +    fun add_inst (c, ty) (terminsts, typinsts) = case local_param thy class c
   3.335 +     of NONE => (terminsts, typinsts)
   3.336 +      | SOME (t, (class', idx)) => (case class_arg c idx ty
   3.337 +         of NONE => (((c, ty), t) :: terminsts, typinsts)
   3.338 +          | SOME ty => (terminsts, add_constrain_classtyp [class'] ty typinsts));
   3.339 +  in pair o (fn ts => let
   3.340 +    val cs = (fold o fold_aterms) (fn Const c_ty => insert (op =) c_ty | _ => I) ts [];
   3.341 +    val (terminsts, typinsts) = fold add_inst cs ([], []);
   3.342 +  in
   3.343 +    ts
   3.344 +    |> (map o map_aterms) (fn t as Const c_ty => the_default t (AList.lookup (op =) terminsts c_ty)
   3.345 +         | t => t)
   3.346 +    |> (map o map_types o map_atyps) (fn t as TFree (v, sort) =>
   3.347 +         case AList.lookup (op =) typinsts v
   3.348 +          of SOME sort' => TFree (v, Sorts.inter_sort algebra (sort, sort'))
   3.349 +           | NONE => t)
   3.350 +  end) end;
   3.351 +
   3.352 +val init_ref = ref (K (pair I) : class -> Proof.context -> (theory -> theory) * Proof.context);
   3.353 +fun init class = ! init_ref class;
   3.354 +
   3.355 +fun init_default class ctxt =
   3.356 +  let
   3.357 +    val thy = ProofContext.theory_of ctxt;
   3.358 +    val term_check = class_term_check thy class;
   3.359 +  in
   3.360 +    ctxt
   3.361 +    (*|> ProofContext.theory_result (remove_constraints class)*)
   3.362 +    |> Context.proof_map (Syntax.add_term_check term_check)
   3.363 +    (*|>> fold (fn (c, ty) => Sign.add_const_constraint_i (c, SOME ty))*)
   3.364 +    |> pair I
   3.365 +  end;
   3.366 +
   3.367  end;
     4.1 --- a/src/Pure/Isar/theory_target.ML	Thu Sep 20 16:37:28 2007 +0200
     4.2 +++ b/src/Pure/Isar/theory_target.ML	Thu Sep 20 16:37:29 2007 +0200
     4.3 @@ -90,14 +90,31 @@
     4.4      fun const_class (SOME class) ((c, _), mx) (_, t) =
     4.5            Class.add_const_in_class class ((c, t), mx)
     4.6        | const_class NONE _ _ = I;
     4.7 -
     4.8 +    fun hide_abbrev (SOME class) abbrs thy =
     4.9 +          let
    4.10 +            val raw_cs = map (fst o fst) abbrs;
    4.11 +            val prfx = (Logic.const_of_class o NameSpace.base) class;
    4.12 +            fun mk_name c =
    4.13 +              let
    4.14 +                val n1 = Sign.full_name thy c;
    4.15 +                val n2 = NameSpace.qualifier n1;
    4.16 +                val n3 = NameSpace.base n1;
    4.17 +              in NameSpace.implode [n2, prfx, prfx, n3] end;
    4.18 +            val cs = map mk_name raw_cs;
    4.19 +          in
    4.20 +            Sign.hide_consts_i true cs thy
    4.21 +          end
    4.22 +      | hide_abbrev NONE _ thy = thy;
    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 +    
    4.27    in
    4.28      lthy'
    4.29 +    |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
    4.30      |> is_loc ? fold (internal_abbrev Syntax.default_mode) abbrs
    4.31 -    |> LocalTheory.raw_theory (fold2 (const_class some_class) decls abbrs)
    4.32 +    |> LocalTheory.raw_theory (hide_abbrev some_class abbrs)
    4.33 +        (*FIXME abbreviations should never occur*)
    4.34      |> LocalDefs.add_defs defs
    4.35      |>> map (apsnd snd)
    4.36    end;
    4.37 @@ -342,10 +359,15 @@
    4.38      val thy = ProofContext.theory_of ctxt;
    4.39      val is_loc = loc <> "";
    4.40      val some_class = Class.class_of_locale thy loc;
    4.41 +    fun class_init_exit (SOME class) =
    4.42 +          Class.init class
    4.43 +      | class_init_exit NONE =
    4.44 +          pair I;
    4.45    in
    4.46      ctxt
    4.47      |> Data.put (if is_loc then SOME loc else NONE)
    4.48 -    |> LocalTheory.init (NameSpace.base loc)
    4.49 +    |> class_init_exit some_class
    4.50 +    |-> (fn exit => LocalTheory.init (NameSpace.base loc)
    4.51       {pretty = pretty loc,
    4.52        consts = consts is_loc some_class,
    4.53        axioms = axioms,
    4.54 @@ -358,8 +380,9 @@
    4.55        target_morphism = target_morphism loc,
    4.56        target_naming = target_naming loc,
    4.57        reinit = fn _ =>
    4.58 -        begin loc o (if is_loc then Locale.init loc else ProofContext.init),
    4.59 -      exit = LocalTheory.target_of}
    4.60 +        (if is_loc then Locale.init loc else ProofContext.init)
    4.61 +        #> begin loc,
    4.62 +      exit = LocalTheory.target_of #> ProofContext.theory exit })
    4.63    end;
    4.64  
    4.65  fun init_i NONE thy = begin "" (ProofContext.init thy)