abbrevs within inductive definitions may no longer depend on each other (reflects in internal organization, particularly for output);
authorwenzelm
Mon Oct 22 15:24:58 2007 +0200 (2007-10-22)
changeset 251432a1acc88a180
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
src/HOL/Tools/inductive_package.ML
     1.1 --- a/src/HOL/Bali/DeclConcepts.thy	Mon Oct 22 15:24:55 2007 +0200
     1.2 +++ b/src/HOL/Bali/DeclConcepts.thy	Mon Oct 22 15:24:58 2007 +0200
     1.3 @@ -794,8 +794,7 @@
     1.4  where
     1.5    "G\<turnstile>membr of cls accessible_from accclass \<equiv> accessible_fromR G accclass membr cls"
     1.6  
     1.7 -| "G\<turnstile>Method m of cls accessible_from accclass \<equiv>
     1.8 -   G\<turnstile>methdMembr m of cls accessible_from accclass"  
     1.9 +| "G\<turnstile>Method m of cls accessible_from accclass \<equiv> accessible_fromR G accclass (methdMembr m) cls"
    1.10  
    1.11  | Immediate:  "\<lbrakk>G\<turnstile>membr member_of class;
    1.12                  G\<turnstile>(Class class) accessible_in (pid accclass);
    1.13 @@ -838,8 +837,7 @@
    1.14  where
    1.15    "G\<turnstile>membr in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC membr C"
    1.16  
    1.17 -| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv>
    1.18 -   G\<turnstile>methdMembr m in C dyn_accessible_from accC"
    1.19 +| "G\<turnstile>Method m in C dyn_accessible_from accC \<equiv> dyn_accessible_fromR G accC (methdMembr m) C"
    1.20  
    1.21  | Immediate:  "\<lbrakk>G\<turnstile>membr member_in class;
    1.22                  G\<turnstile>membr in class permits_acc_from accclass 
     2.1 --- a/src/HOL/Tools/inductive_package.ML	Mon Oct 22 15:24:55 2007 +0200
     2.2 +++ b/src/HOL/Tools/inductive_package.ML	Mon Oct 22 15:24:58 2007 +0200
     2.3 @@ -813,10 +813,10 @@
     2.4      val cs = map (Free o fst) cnames_syn';
     2.5      val ps = map Free pnames;
     2.6  
     2.7 -    val ctxt2 = lthy
     2.8 -      |> Variable.add_fixes (map (fst o fst) cnames_syn') |> snd
     2.9 -      |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
    2.10 -    val expand = Assumption.export_term ctxt2 lthy #> ProofContext.cert_term lthy;
    2.11 +    val (_, ctxt2) = lthy |> Variable.add_fixes (map (fst o fst) cnames_syn');
    2.12 +    val _ = map (fn abbr => LocalDefs.fixed_abbrev abbr ctxt2) abbrevs;
    2.13 +    val ctxt3 = ctxt2 |> fold (snd oo LocalDefs.fixed_abbrev) abbrevs;
    2.14 +    val expand = Assumption.export_term ctxt3 lthy #> ProofContext.cert_term lthy;
    2.15  
    2.16      fun close_rule r = list_all_free (rev (fold_aterms
    2.17        (fn t as Free (v as (s, _)) =>