Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
authorwenzelm
Mon, 22 Oct 2007 15:24:58 +0200
changeset 25143 2a1acc88a180
parent 25142 57c717b9dd59
child 25144 5157a76559b6
abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
src/HOL/Bali/DeclConcepts.thy file | annotate | diff | comparison | revisions
src/HOL/Tools/inductive_package.ML file | annotate | diff | comparison | revisions 
--- 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 
--- 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, _)) =>
isabelle