# HG changeset patch
# User ballarin
# Date 1228742309 -3600
# Node ID 8e7d6f959bd74a57d486f2f009f25f1fe29720e7
# Parent  17538bdef54697dc6f8d7b1074dae5feb27d3fdb
Explicitly close up defines.

diff -r 17538bdef546 -r 8e7d6f959bd7 src/FOL/ex/NewLocaleTest.thy
--- a/src/FOL/ex/NewLocaleTest.thy	Fri Dec 05 16:41:36 2008 +0100
+++ b/src/FOL/ex/NewLocaleTest.thy	Mon Dec 08 14:18:29 2008 +0100
@@ -113,6 +113,18 @@
 print_locale! use_decl thm use_decl_def
 
 
+text {* Defines *}
+
+locale logic_def =
+  fixes land (infixl "&&" 55)
+    and lor (infixl "||" 50)
+    and lnot ("-- _" [60] 60)
+  assumes assoc: "(x && y) && z = x && (y && z)"
+    and notnot: "-- (-- x) = x"
+  defines "x || y == --(-- x && -- y)"
+
+print_locale! logic_def
+
 text {* Theorem statements *}
 
 lemma (in lgrp) lcancel:
diff -r 17538bdef546 -r 8e7d6f959bd7 src/Pure/Isar/expression.ML
--- a/src/Pure/Isar/expression.ML	Fri Dec 05 16:41:36 2008 +0100
+++ b/src/Pure/Isar/expression.ML	Mon Dec 08 14:18:29 2008 +0100
@@ -370,6 +370,7 @@
               Term.fold_aterms (fn Free (x, T) =>
                 if AList.defined (op =) parms x then I else insert (op =) (x, T) | _ => I) t [];
           in Term.list_all_free (rev rev_frees, t) end;
+  (* FIXME consider closing in syntactic phase *)
 
         fun no_binds [] = []
           | no_binds _ = error "Illegal term bindings in context element";
@@ -378,7 +379,7 @@
           Assumes asms => Assumes (asms |> map (fn (a, propps) =>
             (a, map (fn (t, ps) => (close_frees t, no_binds ps)) propps)))
         | Defines defs => Defines (defs |> map (fn (a, (t, ps)) =>
-            (a, (close_frees (#2 (LocalDefs.cert_def ctxt t)), no_binds ps))))
+            (a, (close_frees (#2 (LocalDefs.cert_def ctxt (close_frees t))), no_binds ps))))
         | e => e)
       end;
 
diff -r 17538bdef546 -r 8e7d6f959bd7 src/Pure/Isar/new_locale.ML
--- a/src/Pure/Isar/new_locale.ML	Fri Dec 05 16:41:36 2008 +0100
+++ b/src/Pure/Isar/new_locale.ML	Mon Dec 08 14:18:29 2008 +0100
@@ -353,7 +353,7 @@
 
 fun activate_declarations thy dep ctxt =
   roundup thy activate_decls dep (get_local_idents ctxt, ctxt) |> uncurry put_local_idents;
-  
+
 fun activate_global_facts dep thy =
   roundup thy (activate_notes init_global_elem) dep (get_global_idents thy, thy) |>
   uncurry put_global_idents;