Explicitly close up defines.
authorballarin
Mon Dec 08 14:18:29 2008 +0100 (2008-12-08)
changeset 290198e7d6f959bd7
parent 29018 17538bdef546
child 29020 3e95d28114a1
Explicitly close up defines.
src/FOL/ex/NewLocaleTest.thy
src/Pure/Isar/expression.ML
src/Pure/Isar/new_locale.ML
     1.1 --- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 16:41:36 2008 +0100
     1.2 +++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 14:18:29 2008 +0100
     1.3 @@ -113,6 +113,18 @@
     1.4  print_locale! use_decl thm use_decl_def
     1.5  
     1.6  
     1.7 +text {* Defines *}
     1.8 +
     1.9 +locale logic_def =
    1.10 +  fixes land (infixl "&&" 55)
    1.11 +    and lor (infixl "||" 50)
    1.12 +    and lnot ("-- _" [60] 60)
    1.13 +  assumes assoc: "(x && y) && z = x && (y && z)"
    1.14 +    and notnot: "-- (-- x) = x"
    1.15 +  defines "x || y == --(-- x && -- y)"
    1.16 +
    1.17 +print_locale! logic_def
    1.18 +
    1.19  text {* Theorem statements *}
    1.20  
    1.21  lemma (in lgrp) lcancel:
     2.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 05 16:41:36 2008 +0100
     2.2 +++ b/src/Pure/Isar/expression.ML	Mon Dec 08 14:18:29 2008 +0100
     2.3 @@ -370,6 +370,7 @@
     2.4                Term.fold_aterms (fn Free (x, T) =>
     2.5                  if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
     2.6            in Term.list_all_free (rev rev_frees, t) end;
     2.7 +  (* FIXME consider closing in syntactic phase *)
     2.8  
     2.9          fun no_binds [] = []
    2.10            | no_binds _ = error "Illegal term bindings in context element";
    2.11 @@ -378,7 +379,7 @@
    2.12            Assumes asms => Assumes (asms |> map (fn (a, propps) =>
    2.13              (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
    2.14          | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
    2.15 -            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
    2.16 +            (a, (close_frees (#2 (LocalDefs.cert_def ctxt (close_frees t))), no_binds ps))))
    2.17          | e => e)
    2.18        end;
    2.19  
     3.1 --- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 16:41:36 2008 +0100
     3.2 +++ b/src/Pure/Isar/new_locale.ML	Mon Dec 08 14:18:29 2008 +0100
     3.3 @@ -353,7 +353,7 @@
     3.4  
     3.5  fun activate_declarations thy dep ctxt =
     3.6    roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
     3.7 -  
     3.8 +
     3.9  fun activate_global_facts dep thy =
    3.10    roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
    3.11    uncurry put_global_idents;