# HG changeset patch
# User huffman
# Date 1268503245 28800
# Node ID 500c32e5fadc67a3ec328e1f7d3c7141694ee770
# Parent  cff6dfae284a3e17e60e98dbeddb6c84225d0214
fixrec now generates qualified theorem names

diff -r cff6dfae284a -r 500c32e5fadc src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 09:32:19 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 10:00:45 2010 -0800
@@ -158,13 +158,13 @@
     val unfold_thms = unfolds names tuple_unfold_thm;
     val induct_note : Attrib.binding * Thm.thm list =
       let
-        val thm_name = Binding.name (all_names ^ "_induct");
+        val thm_name = Binding.qualify true all_names (Binding.name "induct");
       in
         ((thm_name, []), [tuple_induct_thm])
       end;
     fun unfold_note (name, thm) : Attrib.binding * Thm.thm list =
       let
-        val thm_name = Binding.name (name ^ "_unfold");
+        val thm_name = Binding.qualify true name (Binding.name "unfold");
         val src = Attrib.internal (K add_unfold);
       in
         ((thm_name, [src]), [thm])
@@ -384,7 +384,7 @@
       val simps : (Attrib.binding * thm) list list =
         map (make_simps lthy') (unfold_thms ~~ blocks);
       fun mk_bind n : Attrib.binding =
-       (Binding.name (n ^ "_simps"),
+       (Binding.qualify true n (Binding.name "simps"),
          [Attrib.internal (K Simplifier.simp_add)]);
       val simps1 : (Attrib.binding * thm list) list =
         map (fn (n,xs) => (mk_bind n, map snd xs)) (names ~~ simps);
@@ -415,7 +415,7 @@
     val eq = mk_trp (HOLogic.eq_const T $ t $ Var (("x",0),T));
     val cname = case chead_of t of Const(c,_) => c | _ =>
               fixrec_err "function is not declared as constant in theory";
-    val unfold_thm = PureThy.get_thm thy (cname^"_unfold");
+    val unfold_thm = PureThy.get_thm thy (cname^".unfold");
     val simp = Goal.prove_global thy [] [] eq
           (fn _ => EVERY [stac unfold_thm 1, simp_tac (global_simpset_of thy) 1]);
   in simp end;
diff -r cff6dfae284a -r 500c32e5fadc src/HOLCF/ex/Powerdomain_ex.thy
--- a/src/HOLCF/ex/Powerdomain_ex.thy	Sat Mar 13 09:32:19 2010 -0800
+++ b/src/HOLCF/ex/Powerdomain_ex.thy	Sat Mar 13 10:00:45 2010 -0800
@@ -85,27 +85,27 @@
 where "tree3 = Node\<cdot>(Node\<cdot>(Leaf\<cdot>(Def 1))\<cdot>tree3)
                    \<cdot>(Node\<cdot>(Leaf\<cdot>(Def 3))\<cdot>(Leaf\<cdot>(Def 4)))"
 
-declare tree1_simps tree2_simps tree3_simps [simp del]
+declare tree1.simps tree2.simps tree3.simps [simp del]
 
 lemma pick_tree1:
   "pick\<cdot>tree1 = {Def 1, Def 2, Def 3, Def 4}\<natural>"
-apply (subst tree1_simps)
+apply (subst tree1.simps)
 apply simp
 apply (simp add: convex_plus_ac)
 done
 
 lemma pick_tree2:
   "pick\<cdot>tree2 = {Def 1, Def 2, \<bottom>, Def 4}\<natural>"
-apply (subst tree2_simps)
+apply (subst tree2.simps)
 apply simp
 apply (simp add: convex_plus_ac)
 done
 
 lemma pick_tree3:
   "pick\<cdot>tree3 = {Def 1, \<bottom>, Def 3, Def 4}\<natural>"
-apply (subst tree3_simps)
+apply (subst tree3.simps)
 apply simp
-apply (induct rule: tree3_induct)
+apply (induct rule: tree3.induct)
 apply simp
 apply simp
 apply (simp add: convex_plus_ac)