# HG changeset patch
# User huffman
# Date 1268505518 28800
# Node ID a57ab2c01369bffbde9fd07d6897d68d546d41e5
# Parent  500c32e5fadc67a3ec328e1f7d3c7141694ee770
fixes to allow using fixrec_simp inside a locale, with test in ex/Fixrec_ex.thy

diff -r 500c32e5fadc -r a57ab2c01369 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 10:00:45 2010 -0800
+++ b/src/HOLCF/Tools/fixrec.ML	Sat Mar 13 10:38:38 2010 -0800
@@ -101,10 +101,10 @@
 
 fun name_of (Const (n, T)) = n
   | name_of (Free (n, T)) = n
-  | name_of _ = fixrec_err "name_of"
+  | name_of t = raise TERM ("Fixrec.add_unfold: lhs not a constant", [t]);
 
 val lhs_name =
-  name_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
+  name_of o head_of o fst o HOLogic.dest_eq o HOLogic.dest_Trueprop o prop_of;
 
 in
 
@@ -311,7 +311,7 @@
       else HOLogic.dest_Trueprop (Logic.strip_imp_concl t);
     fun tac (t, i) =
       let
-        val Const (c, T) = chead_of (fst (HOLogic.dest_eq (concl t)));
+        val Const (c, T) = head_of (chead_of (fst (HOLogic.dest_eq (concl t))));
         val unfold_thm = the (Symtab.lookup tab c);
         val rule = unfold_thm RS @{thm ssubst_lhs};
       in
diff -r 500c32e5fadc -r a57ab2c01369 src/HOLCF/ex/Fixrec_ex.thy
--- a/src/HOLCF/ex/Fixrec_ex.thy	Sat Mar 13 10:00:45 2010 -0800
+++ b/src/HOLCF/ex/Fixrec_ex.thy	Sat Mar 13 10:38:38 2010 -0800
@@ -150,8 +150,8 @@
 and    'a forest = Empty | Trees (lazy "'a tree") "'a forest"
 
 text {*
-  To define mutually recursive functions, separate the equations
-  for each function using the keyword @{text "and"}.
+  To define mutually recursive functions, give multiple type signatures
+  separated by the keyword @{text "and"}.
 *}
 
 fixrec
@@ -173,13 +173,31 @@
 
 text {*
   Theorems generated:
-  @{text map_tree_def}
-  @{text map_forest_def}
-  @{text map_tree_unfold}
-  @{text map_forest_unfold}
-  @{text map_tree_simps}
-  @{text map_forest_simps}
-  @{text map_tree_map_forest_induct}
+  @{text map_tree_def}  @{thm map_tree_def}
+  @{text map_forest_def}  @{thm map_forest_def}
+  @{text map_tree.unfold}  @{thm map_tree.unfold}
+  @{text map_forest.unfold}  @{thm map_forest.unfold}
+  @{text map_tree.simps}  @{thm map_tree.simps}
+  @{text map_forest.simps}  @{thm map_forest.simps}
+  @{text map_tree_map_forest.induct}  @{thm map_tree_map_forest.induct}
 *}
 
+
+subsection {* Using @{text fixrec} inside locales *}
+
+locale test =
+  fixes foo :: "'a \<rightarrow> 'a"
+  assumes foo_strict: "foo\<cdot>\<bottom> = \<bottom>"
+begin
+
+fixrec
+  bar :: "'a u \<rightarrow> 'a"
+where
+  "bar\<cdot>(up\<cdot>x) = foo\<cdot>x"
+
+lemma bar_strict: "bar\<cdot>\<bottom> = \<bottom>"
+by fixrec_simp
+
 end
+
+end