# HG changeset patch
# User wenzelm
# Date 1193059498 -7200
# Node ID 2a1acc88a180c7d95ca8d87e9171593d04603162
# Parent  57c717b9dd59843465f8dd5fd094d2b6c2b89e46
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);

diff -r 57c717b9dd59 -r 2a1acc88a180 src/HOL/Bali/DeclConcepts.thy
--- a/src/HOL/Bali/DeclConcepts.thy	Mon Oct 22 15:24:55 2007 +0200
+++ b/src/HOL/Bali/DeclConcepts.thy	Mon Oct 22 15:24:58 2007 +0200
@@ -794,8 +794,7 @@
 where
   "G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls"
 
-| "G\<turnstile>Method m of cls accessible_from accclass \<equiv>
-   G\<turnstile>methdMembr m of cls accessible_from accclass"  
+| "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
 
 | Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
                 G\<turnstile>(Class class) accessible_in (pid accclass);
@@ -838,8 +837,7 @@
 where
   "G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C"
 
-| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv>
-   G\<turnstile>methdMembr m in C dyn_accessible_from accC"
+| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
 
 | Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
                 G\<turnstile>membr in class permits_acc_from accclass 
diff -r 57c717b9dd59 -r 2a1acc88a180 src/HOL/Tools/inductive_package.ML
--- a/src/HOL/Tools/inductive_package.ML	Mon Oct 22 15:24:55 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 22 15:24:58 2007 +0200
@@ -813,10 +813,10 @@
     val cs = map (Free o fst) cnames_syn';
     val ps = map Free pnames;
 
-    val ctxt2 = lthy
-      |> Variable.add_fixes (map (fst o fst) cnames_syn') |> snd
-      |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
-    val expand = Assumption.export_term ctxt2 lthy #> ProofContext.cert_term lthy;
+    val (_, ctxt2) = lthy |> Variable.add_fixes (map (fst o fst) cnames_syn');
+    val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
+    val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
+    val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
 
     fun close_rule r = list_all_free (rev (fold_aterms
       (fn t as Free (v as (s, _)) =>