1.1 --- a/src/Pure/Isar/theory_target.ML	Fri Feb 23 08:39:25 2007 +0100
     1.2 +++ b/src/Pure/Isar/theory_target.ML	Fri Feb 23 08:39:26 2007 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  signature THEORY_TARGET =
     1.5  sig
     1.6    val peek: local_theory -> string option
     1.7 -  val begin: bool -> bstring -> Proof.context -> local_theory
     1.8 +  val begin: bstring -> Proof.context -> local_theory
     1.9    val init: xstring option -> theory -> local_theory
    1.10    val init_i: string option -> theory -> local_theory
    1.11  end;
    1.12 @@ -60,7 +60,7 @@
    1.13    LocalTheory.term_syntax (ProofContext.target_abbrev prmode ((c, mx), t)) #>
    1.14    ProofContext.add_abbrev Syntax.internalM (c, t) #> snd;
    1.15  
    1.16 -fun consts is_class is_loc depends decls lthy =
    1.17 +fun consts is_loc some_class depends decls lthy =
    1.18    let
    1.19      val xs = filter depends (#1 (ProofContext.inferred_fixes (LocalTheory.target_of lthy)));
    1.20  
    1.21 @@ -68,7 +68,7 @@
    1.22        let
    1.23          val U = map #2 xs ---> T;
    1.24          val t = Term.list_comb (Const (Sign.full_name thy c, U), map Free xs);
    1.25 -        val (mx1, mx2) = ClassPackage.fork_mixfix is_class is_loc mx;
    1.26 +        val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
    1.27          val thy' = Sign.add_consts_authentic [(c, U, mx1)] thy;
    1.28        in (((c, mx2), t), thy') end;
    1.29  
    1.30 @@ -87,7 +87,7 @@
    1.31    #1 (ProofContext.inferred_fixes ctxt)
    1.32    |> filter (member (op =) (fold (Variable.add_fixed ctxt) ts []));
    1.33  
    1.34 -fun abbrev is_class is_loc prmode ((raw_c, mx), raw_t) lthy =
    1.35 +fun abbrev is_loc some_class  prmode ((raw_c, mx), raw_t) lthy =
    1.36    let
    1.37      val thy_ctxt = ProofContext.init (ProofContext.theory_of lthy);
    1.38      val target = LocalTheory.target_of lthy;
    1.39 @@ -102,7 +102,7 @@
    1.40  
    1.41      val ((lhs as Const (full_c, _), rhs), lthy1) = lthy
    1.42        |> LocalTheory.theory_result (Sign.add_abbrev (#1 prmode) (c, u'));
    1.43 -    val (mx1, mx2) = ClassPackage.fork_mixfix is_class is_loc mx;
    1.44 +    val (mx1, mx2) = ClassPackage.fork_mixfix is_loc some_class mx;
    1.45    in
    1.46      lthy1
    1.47      |> LocalTheory.theory (Sign.add_notation prmode [(lhs, mx1)])
    1.48 @@ -129,7 +129,7 @@
    1.49  
    1.50  in
    1.51  
    1.52 -fun defs loc is_class kind args lthy0 =
    1.53 +fun defs loc some_class kind args lthy0 =
    1.54    let
    1.55      fun def ((c, mx), ((name, atts), rhs)) lthy1 =
    1.56        let
    1.57 @@ -147,12 +147,12 @@
    1.58            [(*c == loc.c xs*) lhs_def,
    1.59             (*lhs' == rhs'*)  def,
    1.60             (*rhs' == rhs*)   Thm.symmetric rhs_conv];
    1.61 -        val lthy4 = if is_class
    1.62 -          then
    1.63 -            LocalTheory.raw_theory
    1.64 -              (ClassPackage.add_def_in_class lthy3 loc
    1.65 -                ((c, mx), ((name, atts), (rhs, eq)))) lthy3
    1.66 -          else lthy3;
    1.67 +        val lthy4 = case some_class
    1.68 +         of SOME class => 
    1.69 +              LocalTheory.raw_theory
    1.70 +                (ClassPackage.add_def_in_class lthy3 class
    1.71 +                  ((c, mx), ((name, atts), (rhs, eq)))) lthy3
    1.72 +          | _ => lthy3;
    1.73        in ((lhs, ((name', atts), [([eq], [])])), lthy4) end;
    1.74  
    1.75      val ((lhss, facts), lthy') = lthy0 |> fold_map def args |>> split_list;
    1.76 @@ -298,15 +298,20 @@
    1.77  
    1.78  (* init and exit *)
    1.79  
    1.80 -fun begin is_class loc =
    1.81 -  let val is_loc = loc <> "" in
    1.82 -    Data.put (if is_loc then SOME loc else NONE) #>
    1.83 -    LocalTheory.init (NameSpace.base loc)
    1.84 +fun begin loc ctxt =
    1.85 +  let
    1.86 +    val thy = ProofContext.theory_of ctxt;
    1.87 +    val is_loc = loc <> "";
    1.88 +    val some_class = ClassPackage.class_of_locale thy loc;
    1.89 +  in
    1.90 +    ctxt
    1.91 +    |> Data.put (if is_loc then SOME loc else NONE)
    1.92 +    |> LocalTheory.init (NameSpace.base loc)
    1.93       {pretty = pretty loc,
    1.94 -      consts = consts is_class is_loc,
    1.95 +      consts = consts is_loc some_class,
    1.96        axioms = axioms,
    1.97 -      abbrev = abbrev is_class is_loc,
    1.98 -      defs = defs loc is_class,
    1.99 +      abbrev = abbrev is_loc some_class,
   1.100 +      defs = defs loc some_class,
   1.101        notes = notes loc,
   1.102        type_syntax = type_syntax loc,
   1.103        term_syntax = term_syntax loc,
   1.104 @@ -314,14 +319,12 @@
   1.105        target_morphism = target_morphism loc,
   1.106        target_naming = target_naming loc,
   1.107        reinit = fn _ =>
   1.108 -        begin is_class loc o (if is_loc then Locale.init loc else ProofContext.init),
   1.109 +        begin loc o (if is_loc then Locale.init loc else ProofContext.init),
   1.110        exit = LocalTheory.target_of}
   1.111    end;
   1.112  
   1.113 -fun init_i NONE thy = begin false "" (ProofContext.init thy)
   1.114 -  | init_i (SOME loc) thy =
   1.115 -      begin ((is_some o ClassPackage.class_of_locale thy) loc)
   1.116 -        loc (Locale.init loc thy);
   1.117 +fun init_i NONE thy = begin "" (ProofContext.init thy)
   1.118 +  | init_i (SOME loc) thy = begin loc (Locale.init loc thy);
   1.119  
   1.120  fun init (SOME "-") thy = init_i NONE thy
   1.121    | init loc thy = init_i (Option.map (Locale.intern thy) loc) thy;

     2.1 --- a/src/Pure/Tools/class_package.ML	Fri Feb 23 08:39:25 2007 +0100
     2.2 +++ b/src/Pure/Tools/class_package.ML	Fri Feb 23 08:39:26 2007 +0100
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature CLASS_PACKAGE =
     2.6  sig
     2.7 -  val fork_mixfix: bool -> bool -> mixfix -> mixfix * mixfix
     2.8 +  val fork_mixfix: bool -> string option -> mixfix -> mixfix * mixfix
     2.9  
    2.10    val class: bstring -> class list -> Element.context_i Locale.element list -> theory ->
    2.11      string * Proof.context
    2.12 @@ -44,12 +44,12 @@
    2.13  
    2.14  (** auxiliary **)
    2.15  
    2.16 -fun fork_mixfix is_class is_loc mx =
    2.17 +fun fork_mixfix is_loc some_class mx =
    2.18    let
    2.19      val mx' = Syntax.unlocalize_mixfix mx;
    2.20 -    val mx1 = if is_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
    2.21 -    val mx2 = if is_loc then mx else NoSyn;
    2.22 -  in (mx1, mx2) end;
    2.23 +    val mx_global = if is_some some_class orelse (is_loc andalso mx = mx') then NoSyn else mx';
    2.24 +    val mx_local = if is_loc then mx else NoSyn;
    2.25 +  in (mx_global, mx_local) end;
    2.26  
    2.27  
    2.28  (** AxClasses with implicit parameter handling **)
    2.29 @@ -100,7 +100,7 @@
    2.30      #-> (fn axioms_prop => AxClass.define_class_i (name, superclasses) (map fst cs) axioms_prop
    2.31      #-> (fn class => `(fn thy => AxClass.get_definition thy class)
    2.32      #-> (fn {intro, axioms, ...} => fold (add_constraint class) cs
    2.33 -    #> pair (class, ((intro, (maps snd axioms_prop, axioms)), cs))))))
    2.34 +    #> pair (class, ((intro, (map Thm.prop_of axioms, axioms)), cs))))))
    2.35    end;
    2.36  
    2.37  
    2.38 @@ -471,7 +471,7 @@
    2.39        in
    2.40          (map (fst o fst) params, params
    2.41          |> (map o apfst o apsnd o Term.map_type_tfree) (K (TFree (AxClass.param_tyvarname, Sign.defaultS thy)))
    2.42 -        |> (map o apsnd) (fork_mixfix false true #> fst)
    2.43 +        |> (map o apsnd) (fork_mixfix true NONE #> fst)
    2.44          |> chop (length supconsts)
    2.45          |> snd)
    2.46        end;
    2.47 @@ -501,7 +501,7 @@
    2.48      fun make_witness t thm = Element.make_witness t (Goal.protect thm);
    2.49    in
    2.50      thy
    2.51 -    |> add_locale bname supexpr ((*elems_constrains @*) elems)
    2.52 +    |> add_locale (SOME (bname ^ "_pred")) bname supexpr ((*elems_constrains @*) elems)
    2.53      |-> (fn name_locale => ProofContext.theory_result (
    2.54        `(fn thy => extract_params thy name_locale)
    2.55        #-> (fn (param_names, params) =>
    2.56 @@ -513,7 +513,7 @@
    2.57            (name_locale, map (fst o fst) params ~~ map fst consts,
    2.58              map2 make_witness ax_terms ax_axioms, axiom_names))
    2.59        #> prove_interpretation ((ALLGOALS o ProofContext.fact_tac) ax_axioms)
    2.60 -          (Logic.const_of_class bname, []) (Locale.Locale name_locale)
    2.61 +          ((true, Logic.const_of_class bname), []) (Locale.Locale name_locale)
    2.62            (mk_instT name_axclass, mk_inst name_axclass param_names (map snd supconsts @ consts))
    2.63        #> pair name_axclass
    2.64        )))))
    2.65 @@ -521,8 +521,8 @@
    2.66  
    2.67  in
    2.68  
    2.69 -val class_cmd = gen_class (Locale.add_locale true) read_class;
    2.70 -val class = gen_class (Locale.add_locale_i true) certify_class;
    2.71 +val class_cmd = gen_class Locale.add_locale read_class;
    2.72 +val class = gen_class Locale.add_locale_i certify_class;
    2.73  
    2.74  end; (*local*)
    2.75  
    2.76 @@ -558,11 +558,24 @@
    2.77  
    2.78  (** experimental class target **)
    2.79  
    2.80 -fun add_def_in_class lthy loc ((c, syn), ((name, atts), (rhs, eq))) thy =
    2.81 +fun print_witness wit =
    2.82    let
    2.83 -    val SOME class = class_of_locale thy loc;
    2.84 +    val (t, thm) = Element.dest_witness wit;
    2.85 +    val prop = Thm.prop_of thm;
    2.86 +    fun string_of_tfree (v, sort) = v ^ "::" ^ Display.raw_string_of_sort sort;
    2.87 +    fun string_of_tvar (v, sort) = Library.string_of_indexname v ^ "::" ^ Display.raw_string_of_sort sort;
    2.88 +    fun print_term t =
    2.89 +      let
    2.90 +        val term = Display.raw_string_of_term t;
    2.91 +        val tfrees = map string_of_tfree (Term.add_tfrees t []);
    2.92 +        val tvars = map string_of_tvar (Term.add_tvars t []);
    2.93 +      in term :: tfrees @ tvars end;
    2.94 +  in (map Output.info (print_term t); map Output.info (print_term prop)) end;
    2.95 +
    2.96 +fun add_def_in_class lthy class ((c, syn), ((name, atts), (rhs, eq))) thy =
    2.97 +  let
    2.98      val rhs' = global_term thy [class] rhs;
    2.99 -    val (syn', _) = fork_mixfix true true syn;
   2.100 +    val (syn', _) = fork_mixfix true NONE syn;
   2.101      val ty = Term.fastype_of rhs';
   2.102      fun add_const (c, ty, syn) =
   2.103        Sign.add_consts_authentic [(c, ty, syn)]
   2.104 @@ -581,7 +594,9 @@
   2.105      val witness = the_witness thy class;
   2.106      val _ = Output.info "------ WIT ------";
   2.107      fun print_wit (t, thm) = "(" ^ Sign.string_of_term thy t ^ ", " ^ Display.string_of_thm thm ^ ")"
   2.108 +    fun print_raw_wit (t, thm) = "(" ^ Display.raw_string_of_term t ^ ", " ^ (Display.raw_string_of_term o Thm.prop_of) thm ^ ")"
   2.109      val _ = (Output.info o cat_lines o map (print_wit o Element.dest_witness)) witness;
   2.110 +    val _ = map print_witness witness;
   2.111      val _ = (Output.info o string_of_thm) eq';
   2.112      val eq'' = Element.satisfy_thm witness eq';
   2.113      val _ = (Output.info o string_of_thm) eq'';*)