src/Pure/Thy/thy_read.ML

                                 children: string list,
                                 thy_time: string option,
                                 ml_time: string option,
                                 theory: theory option,
                                 thms: thm Symtab.table,
-                                thy_simps: thm list, ml_simps: thm list};
+                                thy_ss: Simplifier.simpset option,
+                                simpset: Simplifier.simpset option};
       (*meaning of special values:
         thy_time, ml_time = None     theory file has not been read yet
                           = Some ""  theory was read but has either been marked
                                      as outdated or there is no such file for
                                      this theory (see e.g. 'virtual' theories

   val qed_goal: string -> theory -> string -> (thm list -> tactic list) -> unit
   val qed_goalw: string -> theory->thm list->string->(thm list->tactic list)
                  -> unit
   val get_thm: theory -> string -> thm
   val thms_of: theory -> (string * thm) list
+  val simpset_of: string -> Simplifier.simpset
   val print_theory: theory -> unit
 end;
 
 
-functor ReadthyFUN(structure ThySyn: THY_SYN and ThmDB: THMDB
-                   and Simplifier: SIMPLIFIER): READTHY =
+functor ReadthyFun(structure ThySyn: THY_SYN and ThmDB: THMDB): READTHY =
 struct
 
 open ThmDB Simplifier;
 
 datatype basetype = Thy  of string

                                      ThyInfo {path = "",
                                        children = ["Pure", "CPure"],
                                        thy_time = Some "", ml_time = Some "",
                                        theory = Some proto_pure_thy,
                                        thms = Symtab.null,
-                                       thy_simps = [], ml_simps = []}),
+                                       thy_ss = None, simpset = None}),
                                     ("Pure", ThyInfo {path = "", children = [],
                                        thy_time = Some "", ml_time = Some "",
                                        theory = Some pure_thy,
                                        thms = Symtab.null,
-                                       thy_simps = [], ml_simps = []}),
+                                       thy_ss = None, simpset = None}),
                                     ("CPure", ThyInfo {path = "",
                                        children = [],
                                        thy_time = Some "", ml_time = Some "",
                                        theory = Some cpure_thy,
                                        thms = Symtab.null,
-                                       thy_simps = [], ml_simps = []})]);
+                                       thy_ss = None, simpset = None})
+                                   ]);
 
 val loadpath = ref ["."];           (*default search path for theory files *)
 
 val delete_tmpfiles = ref true;         (*remove temporary files after use *)
 

           else
             (false, false)
        end
     | None => (false, false)
 
-(*Get list of simplifiers defined in .thy and .ML file*)
-fun get_simps tname =
-  case get_thyinfo tname of
-      Some (ThyInfo {thy_simps, ml_simps, ...}) => (thy_simps, ml_simps)
-    | None => ([], []);
-
 (*Get all direct ancestors of a theory*)
 fun get_parents child =
   let fun has_child (tname, ThyInfo {children, theory, ...}) = 
         if child mem children then Some tname else None;
   in mapfilter has_child (Symtab.dest (!loaded_thys)) end;
+
+(*Get all descendants of a theory list *)
+fun get_descendants [] = []
+  | get_descendants (t :: ts) =
+      let val tinfo = get_thyinfo t
+      in if is_some tinfo then
+           let val ThyInfo {children, ...} = the tinfo
+           in children union (get_descendants (children union ts))
+           end
+         else []
+      end;
 
 (*Get theory object for a loaded theory *)
 fun get_theory name =
   let val ThyInfo {theory, ...} = the (get_thyinfo name)
   in the theory end;

   end;
 
 (*Remove theory from all child lists in loaded_thys *)
 fun unlink_thy tname =
   let fun remove (ThyInfo {path, children, thy_time, ml_time, theory, thms,
-                           thy_simps, ml_simps}) =
+                           thy_ss, simpset}) =
         ThyInfo {path = path, children = children \ tname,
                  thy_time = thy_time, ml_time = ml_time, theory = theory, 
-                 thms = thms, thy_simps = thy_simps, ml_simps = ml_simps}
+                 thms = thms, thy_ss = thy_ss, simpset = simpset}
   in loaded_thys := Symtab.map remove (!loaded_thys) end;
 
 (*Remove a theory from loaded_thys *)
 fun remove_thy tname =
   loaded_thys := Symtab.make (filter_out (fn (id, _) => id = tname)
                  (Symtab.dest (!loaded_thys)));
 
 (*Change thy_time and ml_time for an existent item *)
-fun set_info thy_time ml_time tname =
-  let val ThyInfo {path, children, theory, thms, thy_simps, ml_simps, ...} =
-        the (Symtab.lookup (!loaded_thys, tname));
-  in loaded_thys := Symtab.update
-       ((tname,
-         ThyInfo {path = path, children = children, thy_time = thy_time,
-                  ml_time = ml_time, theory = theory, thms = thms,
-                  thy_simps = thy_simps, ml_simps = ml_simps}),
-        !loaded_thys)
+fun set_info tname thy_time ml_time =
+  let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
+          Some (ThyInfo {path, children, theory, thms, thy_ss, simpset,...}) =>
+            ThyInfo {path = path, children = children,
+                     thy_time = thy_time, ml_time = ml_time,
+                     theory = theory, thms = thms,
+                     thy_ss = thy_ss, simpset = simpset}
+        | None => ThyInfo {path = "", children = [],
+                           thy_time = thy_time, ml_time = ml_time,
+                           theory = None, thms = Symtab.null,
+                           thy_ss = None, simpset = None};
+  in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
   end;
 
 (*Mark theory as changed since last read if it has been completly read *)
 fun mark_outdated tname =
   let val t = get_thyinfo tname;
   in if is_none t then ()
      else let val ThyInfo {thy_time, ml_time, ...} = the t
-          in set_info (if is_none thy_time then None else Some "")
+          in set_info tname
+                      (if is_none thy_time then None else Some "")
                       (if is_none ml_time then None else Some "")
-                      tname
+                      
           end
   end;
 
 (*Read .thy and .ML files that haven't been read yet or have changed since
   they were last read;

     val (path, tname) = split_filename name;
     val (thy_file, ml_file) = get_filenames path tname;
     val (abs_path, _) = if thy_file = "" then split_filename ml_file
                         else split_filename thy_file;
     val (thy_uptodate, ml_uptodate) = thy_unchanged tname thy_file ml_file;
-    val (thy_simps, ml_simps) = get_simps tname;
-    val old_simps = ref [];
 
     (*Set absolute path for loaded theory *)
     fun set_path () =
-      let val ThyInfo {children, thy_time, ml_time, theory, thms,
-                       thy_simps, ml_simps, ...} =
+      let val ThyInfo {children, thy_time, ml_time, theory, thms, thy_ss,
+                       simpset, ...} =
             the (Symtab.lookup (!loaded_thys, tname));
       in loaded_thys := Symtab.update ((tname,
                           ThyInfo {path = abs_path, children = children,
                                    thy_time = thy_time, ml_time = ml_time,
                                    theory = theory, thms = thms,
-                                   thy_simps = thy_simps,
-                                   ml_simps = ml_simps}),
+                                   thy_ss = thy_ss, simpset = simpset}),
                           !loaded_thys)
       end;
 
     (*Mark all direct descendants of a theory as changed *)
     fun mark_children thy =

 
     (*Remove theorems associated with a theory*)
     fun delete_thms () =
       let
         val tinfo = case get_thyinfo tname of
-            Some (ThyInfo {path, children, thy_time, ml_time, theory,
-                           thy_simps, ml_simps, ...}) =>
-                ThyInfo {path = path, children = children,
-                         thy_time = thy_time, ml_time = ml_time,
-                         theory = theory, thms = Symtab.null,
-                         thy_simps = thy_simps, ml_simps = ml_simps}
+            Some (ThyInfo {path, children, thy_time, ml_time, theory, thy_ss,
+                           simpset, ...}) =>
+              ThyInfo {path = path, children = children,
+                       thy_time = thy_time, ml_time = ml_time,
+                       theory = theory, thms = Symtab.null,
+                       thy_ss = thy_ss, simpset = simpset}
           | None => ThyInfo {path = "", children = [],
                              thy_time = None, ml_time = None,
                              theory = None, thms = Symtab.null,
-                             thy_simps = [], ml_simps = []};
-      in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys) end;
-
-    fun update_simps (new_thy_simps, new_ml_simps) =
+                             thy_ss = None, simpset = None};
+
+        val ThyInfo {theory, ...} = tinfo;
+      in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys);
+         case theory of
+             Some t => delete_thm_db t
+           | None => ()
+      end;
+
+    fun save_thy_ss () =
       let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
-                       thy_simps, ml_simps} = the (get_thyinfo tname);
-
-          val (thy_simps',  ml_simps') =
-            (if is_none new_thy_simps then thy_simps else the new_thy_simps,
-             if is_none new_ml_simps then ml_simps else the new_ml_simps);
-      in loaded_thys := Symtab.update ((tname,
-           ThyInfo {path = path, children = children,
-                    thy_time = thy_time, ml_time = ml_time, theory = theory,
-                    thms = thms, thy_simps = thy_simps',
-                    ml_simps = ml_simps'}), !loaded_thys)
+                       simpset, ...} = the (get_thyinfo tname);
+      in loaded_thys := Symtab.update
+           ((tname, ThyInfo {path = path, children = children,
+                             thy_time = thy_time, ml_time = ml_time,
+                             theory = theory, thms = thms,
+                             thy_ss = Some (!Simplifier.simpset),
+                             simpset = simpset}),
+            !loaded_thys)
+      end;
+
+    fun save_simpset () =
+      let val ThyInfo {path, children, thy_time, ml_time, theory, thms,
+                       thy_ss, ...} = the (get_thyinfo tname);
+      in loaded_thys := Symtab.update
+           ((tname, ThyInfo {path = path, children = children,
+                             thy_time = thy_time, ml_time = ml_time,
+                             theory = theory, thms = thms,
+                             thy_ss = thy_ss,
+                             simpset = Some (!Simplifier.simpset)}),
+            !loaded_thys)
       end;
 
   in if thy_uptodate andalso ml_uptodate then ()
      else
      (
-       delete_thms ();
-
-       if thy_uptodate orelse thy_file = "" then
-         (Delsimps ml_simps;
-          old_simps := #simps(rep_ss (!simpset));
-          update_simps (None, Some []))
+       if thy_file = "" then ()
+       else if thy_uptodate then
+         simpset := let val ThyInfo {thy_ss, ...} = the (get_thyinfo tname);
+                    in the thy_ss end
        else
          (writeln ("Reading \"" ^ name ^ ".thy\"");
-          Delsimps (thy_simps @ ml_simps);
-          old_simps := #simps(rep_ss (!simpset));
-          update_simps (Some [], Some []);  (*clear simp lists in case use_thy
-                                              encounters an EROR exception*)
+          delete_thms ();
           read_thy tname thy_file;
           use (out_name tname);
+          save_thy_ss ();
 
           if not (!delete_tmpfiles) then ()
-          else delete_file (out_name tname);
-
-          update_simps
-            (Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)),
-             None);
-          old_simps := #simps(rep_ss (!simpset))
+          else delete_file (out_name tname)
          );
 
-       set_info (Some (file_info thy_file)) None tname;
+       set_info tname (Some (file_info thy_file)) None;
                                        (*mark thy_file as successfully loaded*)
 
        if ml_file = "" then ()
-       else
-         (writeln ("Reading \"" ^ name ^ ".ML\"");
-          use ml_file;
-
-          update_simps (None,
-            Some (gen_rems same_thm (#simps(rep_ss (!simpset)), !old_simps)))
-         );
-
-         use_string
-           ["val _ = (store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");\
-            \map store_thm_db (axioms_of " ^ tname ^ ".thy));"];
-                    (*Store theory again because it could have been redefined*)
+       else (writeln ("Reading \"" ^ name ^ ".ML\"");
+             use ml_file);
+       save_simpset ();
+
+       (*Store theory again because it could have been redefined*)
+       use_string
+         ["val _ = store_theory (" ^ tname ^ ".thy, " ^ quote tname ^ ");"];
+
+       (*Store axioms of theory
+         (but only if it's not a copy of an older theory)*)
+       let val parents = get_parents tname;
+           val fst_thy = get_theory (hd parents);
+           val this_thy = get_theory tname;
+           val axioms =
+             if length parents = 1
+                andalso Sign.eq_sg (sign_of fst_thy, sign_of this_thy) then []
+             else axioms_of this_thy;
+       in map store_thm_db axioms end;
 
        (*Now set the correct info*)
-       set_info (Some (file_info thy_file)) (Some (file_info ml_file)) tname;
+       set_info tname (Some (file_info thy_file)) (Some (file_info ml_file));
        set_path ();
 
        (*Mark theories that have to be reloaded*)
        mark_children tname
       )

         | reload_changed [] = ();
 
      (*Remove all theories that are no descendants of ProtoPure.
        If there are still children in the deleted theory's list
        schedule them for reloading *)
-     fun collect_garbage not_garbage =
+     fun collect_garbage no_garbage =
        let fun collect ((tname, ThyInfo {children, ...}) :: ts) =
-                 if tname mem not_garbage then collect ts
+                 if tname mem no_garbage then collect ts
                  else (writeln ("Theory \"" ^ tname ^
                        "\" is no longer linked with ProtoPure - removing it.");
                        remove_thy tname;
                        seq mark_outdated children)
              | collect [] = ()
-
        in collect (Symtab.dest (!loaded_thys)) end;
   in collect_garbage ("ProtoPure" :: (load_order ["ProtoPure"] []));
      reload_changed (load_order ["Pure", "CPure"] [])
   end;
 
 (*Merge theories to build a base for a new theory.
-  Base members are only loaded if they are missing. *)
+  Base members are only loaded if they are missing.*)
 fun mk_base bases child mk_draft =
-      let (*List all descendants of a theory list *)
-          fun list_descendants (t :: ts) =
-                let val tinfo = get_thyinfo t
-                in if is_some tinfo then
-                     let val ThyInfo {children, ...} = the tinfo
-                     in children union (list_descendants (ts union children))
-                     end
-                   else []
-                end
-            | list_descendants [] = [];
-
-          (*Show the cycle that would be created by add_child *)
-          fun show_cycle base =
-            let fun find_it result curr =
-                  let val tinfo = get_thyinfo curr
-                  in if base = curr then
-                       error ("Cyclic dependency of theories: "
-                              ^ child ^ "->" ^ base ^ result)
-                     else if is_some tinfo then
-                       let val ThyInfo {children, ...} = the tinfo
-                       in seq (find_it ("->" ^ curr ^ result)) children
-                       end
-                     else ()
-                  end
-            in find_it "" child end;
-
-          (*Check if a cycle would be created by add_child *)
-          fun find_cycle base =
-            if base mem (list_descendants [child]) then show_cycle base
-            else ();
-
-          (*Add child to child list of base *)
-          fun add_child base =
-            let val tinfo =
-                  case Symtab.lookup (!loaded_thys, base) of
-                      Some (ThyInfo {path, children, thy_time, ml_time,
-                                     theory, thms, thy_simps, ml_simps}) =>
-                        ThyInfo {path = path, children = child ins children,
-                                 thy_time = thy_time, ml_time = ml_time,
-                                 theory = theory, thms = thms,
-                                 thy_simps = thy_simps, ml_simps = ml_simps}
-                    | None => ThyInfo {path = "", children = [child],
-                                       thy_time = None, ml_time = None,
-                                       theory = None, thms = Symtab.null,
-                                       thy_simps = [], ml_simps = []};
-            in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
-
-          (*Load a base theory if not already done
-            and no cycle would be created *)
-          fun load base =
-              let val thy_loaded = already_loaded base
-                                           (*test this before child is added *)
-              in
-                if child = base then
-                    error ("Cyclic dependency of theories: " ^ child
-                           ^ "->" ^ child)
-                else
-                  (find_cycle base;
-                   add_child base;
-                   if thy_loaded then ()
-                   else (writeln ("Autoloading theory " ^ (quote base)
-                                  ^ " (used by " ^ (quote child) ^ ")");
-                         use_thy base)
-                  )
-              end;
-
-          (*Load all needed files and make a list of all real theories *)
-          fun load_base (Thy b :: bs) =
-               (load b;
-                b :: (load_base bs))
-            | load_base (File b :: bs) =
-               (load b;
-                load_base bs)                    (*don't add it to mergelist *)
-            | load_base [] = [];
-
-          val mergelist = (unlink_thy child;
-                           load_base bases);
-     in writeln ("Loading theory " ^ (quote child));
-        merge_thy_list mk_draft (map get_theory mergelist) end;
+  let (*Show the cycle that would be created by add_child *)
+      fun show_cycle base =
+        let fun find_it result curr =
+              let val tinfo = get_thyinfo curr
+              in if base = curr then
+                   error ("Cyclic dependency of theories: "
+                          ^ child ^ "->" ^ base ^ result)
+                 else if is_some tinfo then
+                   let val ThyInfo {children, ...} = the tinfo
+                   in seq (find_it ("->" ^ curr ^ result)) children
+                   end
+                 else ()
+              end
+        in find_it "" child end;
+
+      (*Check if a cycle would be created by add_child *)
+      fun find_cycle base =
+        if base mem (get_descendants [child]) then show_cycle base
+        else ();
+
+      (*Add child to child list of base *)
+      fun add_child base =
+        let val tinfo =
+              case Symtab.lookup (!loaded_thys, base) of
+                  Some (ThyInfo {path, children, thy_time, ml_time,
+                           theory, thms, thy_ss, simpset}) =>
+                    ThyInfo {path = path, children = child ins children,
+                             thy_time = thy_time, ml_time = ml_time,
+                             theory = theory, thms = thms,
+                             thy_ss = thy_ss, simpset = simpset}
+                | None => ThyInfo {path = "", children = [child],
+                                   thy_time = None, ml_time = None,
+                                   theory = None, thms = Symtab.null,
+                                   thy_ss = None, simpset = None};
+        in loaded_thys := Symtab.update ((base, tinfo), !loaded_thys) end;
+
+      (*Load a base theory if not already done
+        and no cycle would be created *)
+      fun load base =
+          let val thy_loaded = already_loaded base
+                                       (*test this before child is added *)
+          in
+            if child = base then
+                error ("Cyclic dependency of theories: " ^ child
+                       ^ "->" ^ child)
+            else
+              (find_cycle base;
+               add_child base;
+               if thy_loaded then ()
+               else (writeln ("Autoloading theory " ^ (quote base)
+                              ^ " (used by " ^ (quote child) ^ ")");
+                     use_thy base)
+              )
+          end;
+
+      (*Get simpset for a theory*)
+      fun get_simpset tname =
+        let val ThyInfo {simpset, ...} = the (get_thyinfo tname);
+        in simpset end;
+
+      (*Load all needed files and make a list of all real theories *)
+      fun load_base (Thy b :: bs) =
+           (load b;
+            b :: (load_base bs))
+        | load_base (File b :: bs) =
+           (load b;
+            load_base bs)                    (*don't add it to mergelist *)
+        | load_base [] = [];
+
+      val dummy = unlink_thy child;
+      val mergelist = load_base bases;
+
+      val base_thy = (writeln ("Loading theory " ^ (quote child));
+                      merge_thy_list mk_draft (map get_theory mergelist));
+ in simpset := foldr merge_ss (mapfilter get_simpset mergelist, empty_ss);
+    base_thy
+ end;
 
 (*Change theory object for an existent item of loaded_thys
-  or create a new item; also store axioms in Thm database*)
+  or create a new item*)
 fun store_theory (thy, tname) =
   let val tinfo = case Symtab.lookup (!loaded_thys, tname) of
                Some (ThyInfo {path, children, thy_time, ml_time, thms,
-                              thy_simps, ml_simps, ...}) =>
+                              thy_ss, simpset, ...}) =>
                  ThyInfo {path = path, children = children,
                           thy_time = thy_time, ml_time = ml_time,
                           theory = Some thy, thms = thms,
-                          thy_simps = thy_simps, ml_simps = ml_simps}
+                          thy_ss = thy_ss, simpset = simpset}
              | None => ThyInfo {path = "", children = [],
                                 thy_time = None, ml_time = None,
                                 theory = Some thy, thms = Symtab.null,
-                                thy_simps = [], ml_simps = []};
+                                thy_ss = None, simpset = None};
   in loaded_thys := Symtab.update ((tname, tinfo), !loaded_thys)
   end;
 
 
 (** store and retrieve theorems **)

 
 (*Store a theorem in the thy_info of its theory*)
 fun store_thm (name, thm) =
   let
     val (thy_name, ThyInfo {path, children, thy_time, ml_time, theory, thms,
-                            thy_simps, ml_simps}) =
+                            thy_ss, simpset}) =
       thyinfo_of_sign (#sign (rep_thm thm));
 
-    val thms' = Symtab.update_new ((name, thm), thms)
+    val (thms', duplicate) = (Symtab.update_new ((name, thm), thms), false)
       handle Symtab.DUPLICATE s => 
-        (if same_thm (the (Symtab.lookup (thms, name)), thm) then 
+        (if eq_thm (the (Symtab.lookup (thms, name)), thm) then 
            (writeln ("Warning: Theory database already contains copy of\
                      \ theorem " ^ quote name);
-            thms)
+            (thms, true))
          else error ("Duplicate theorem name " ^ quote s
                      ^ " used in theory database"));
   in
     loaded_thys := Symtab.update
      ((thy_name, ThyInfo {path = path, children = children,
                           thy_time = thy_time, ml_time = ml_time,
                           theory = theory, thms = thms',
-                          thy_simps = thy_simps, ml_simps = ml_simps}),
+                          thy_ss = thy_ss, simpset = simpset}),
       !loaded_thys);
-    store_thm_db (name, thm)
+    if duplicate then thm else store_thm_db (name, thm)
   end;
 
 (*Store result of proof in loaded_thys and as ML value*)
 
 val qed_thm = ref flexpair_def(*dummy*);

 
 
 (* Retrieve theorems *)
 
 (*Get all theorems belonging to a given theory*)
-fun thmtab_ofthy thy =
+fun thmtab_of_thy thy =
   let val (_, ThyInfo {thms, ...}) = thyinfo_of_sign (sign_of thy);
   in thms end;
 
-fun thmtab_ofname name =
+fun thmtab_of_name name =
   let val ThyInfo {thms, ...} = the (get_thyinfo name);
   in thms end;
 
 (*Get a stored theorem specified by theory and name*)
 fun get_thm thy name =
   let fun get [] [] searched =
            raise THEORY ("get_thm: no theorem " ^ quote name, [thy])
         | get [] ng searched =
             get (ng \\ searched) [] searched
         | get (t::ts) ng searched =
-            (case Symtab.lookup (thmtab_ofname t, name) of
+            (case Symtab.lookup (thmtab_of_name t, name) of
                  Some thm => thm
                | None => get ts (ng union (get_parents t)) (t::searched));
 
       val (tname, _) = thyinfo_of_sign (sign_of thy);
   in get [tname] [] [] end;
 
 (*Get stored theorems of a theory*)
-val thms_of = Symtab.dest o thmtab_ofthy;
-
+val thms_of = Symtab.dest o thmtab_of_thy;
+
+(*Get simpset of a theory*)
+fun simpset_of tname =
+  case get_thyinfo tname of
+      Some (ThyInfo {simpset, ...}) =>
+        if is_some simpset then the simpset
+        else error ("Simpset of theory " ^ tname ^ " has not been stored yet")
+    | None => error ("Theory " ^ tname ^ " not stored by loader");
 
 (* print theory *)
 
 fun print_thms thy =
   let