# HG changeset patch
# User wenzelm
# Date 1461523044 -7200
# Node ID 1fbad761c1bad8d9987a75a37cee8d9f9032de2d
# Parent  b8b672f70d7662eeba11aeb1a15e0783994e21a6
within a proof body context, undeclared frees are like global constants;
tuned signature;

diff -r b8b672f70d76 -r 1fbad761c1ba src/HOL/Tools/Lifting/lifting_setup.ML
--- a/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Apr 24 20:29:49 2016 +0200
+++ b/src/HOL/Tools/Lifting/lifting_setup.ML	Sun Apr 24 20:37:24 2016 +0200
@@ -93,7 +93,7 @@
         ((Binding.empty, []), definition_term)) lthy |>> (snd #> snd);
     fun raw_def lthy =
       let
-        val ((_, rhs), prove) = Local_Defs.derived_def lthy true definition_term;
+        val ((_, rhs), prove) = Local_Defs.derived_def lthy {conditional = true} definition_term;
         val ((_, (_, raw_th)), lthy) = lthy
           |> Local_Theory.define ((Binding.concealed pcrel_name, NoSyn), ((Binding.empty, []), rhs));
         val th = prove lthy raw_th;
diff -r b8b672f70d76 -r 1fbad761c1ba src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Apr 24 20:29:49 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Sun Apr 24 20:37:24 2016 +0200
@@ -28,7 +28,7 @@
   val unfold_tac: Proof.context -> thm list -> tactic
   val fold: Proof.context -> thm list -> thm -> thm
   val fold_tac: Proof.context -> thm list -> tactic
-  val derived_def: Proof.context -> bool -> term ->
+  val derived_def: Proof.context -> {conditional: bool} -> term ->
     ((string * typ) * term) * (Proof.context -> thm -> thm)
 end;
 
@@ -44,9 +44,10 @@
     fun err msg =
       cat_error msg ("The error(s) above occurred in definition:\n" ^
         quote (Syntax.string_of_term ctxt eq));
+    val is_fixed = if Variable.is_body ctxt then NONE else SOME (Variable.is_fixed ctxt);
     val ((lhs, _), eq') = eq
       |> Sign.no_vars ctxt
-      |> Primitive_Defs.dest_def ctxt Term.is_Free (Variable.is_fixed ctxt) (K true)
+      |> Primitive_Defs.dest_def ctxt Term.is_Free is_fixed (K true)
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
@@ -206,7 +207,7 @@
 
 (* derived defs -- potentially within the object-logic *)
 
-fun derived_def ctxt conditional prop =
+fun derived_def ctxt {conditional} prop =
   let
     val ((c, T), rhs) = prop
       |> Thm.cterm_of ctxt
@@ -215,7 +216,8 @@
       |> conditional ? Logic.strip_imp_concl
       |> (abs_def o #2 o cert_def ctxt);
     fun prove ctxt' def =
-      Goal.prove ctxt' (Variable.add_free_names ctxt' prop []) [] prop
+      Goal.prove ctxt'
+        ((not (Variable.is_body ctxt') ? Variable.add_free_names ctxt' prop) []) [] prop
         (fn {context = ctxt'', ...} =>
           ALLGOALS
             (CONVERSION (meta_rewrite_conv ctxt'') THEN'
diff -r b8b672f70d76 -r 1fbad761c1ba src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Apr 24 20:29:49 2016 +0200
+++ b/src/Pure/Isar/specification.ML	Sun Apr 24 20:37:24 2016 +0200
@@ -237,7 +237,7 @@
   let
     val ((vars, [((raw_name, atts), prop)]), get_pos) =
       fst (prep (the_list raw_var) [raw_spec] lthy);
-    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy true prop;
+    val (((x, T), rhs), prove) = Local_Defs.derived_def lthy {conditional = true} prop;
     val _ = Name.reject_internal (x, []);
     val (b, mx) =
       (case vars of
diff -r b8b672f70d76 -r 1fbad761c1ba src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Sun Apr 24 20:29:49 2016 +0200
+++ b/src/Pure/primitive_defs.ML	Sun Apr 24 20:37:24 2016 +0200
@@ -6,7 +6,7 @@
 
 signature PRIMITIVE_DEFS =
 sig
-  val dest_def: Proof.context -> (term -> bool) -> (string -> bool) -> (string -> bool) ->
+  val dest_def: Proof.context -> (term -> bool) -> (string -> bool) option -> (string -> bool) ->
     term -> (term * term) * term
   val abs_def: term -> term * term
 end;
@@ -36,7 +36,7 @@
     val head_tfrees = Term.add_tfrees head [];
 
     fun check_arg (Bound _) = true
-      | check_arg (Free (x, _)) = not (is_fixed x)
+      | check_arg (Free (x, _)) = is_none is_fixed orelse not (the is_fixed x)
       | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
@@ -45,7 +45,7 @@
     val lhs_bads = filter_out check_arg args;
     val lhs_dups = duplicates (op aconv) args;
     val rhs_extras = Term.fold_aterms (fn v as Free (x, _) =>
-      if is_fixed x orelse member (op aconv) args v then I
+      if is_none is_fixed orelse the is_fixed x orelse member (op aconv) args v then I
       else insert (op aconv) v | _ => I) rhs [];
     val rhs_extrasT = Term.fold_aterms (Term.fold_types (fn v as TFree (a, S) =>
       if is_fixedT a orelse member (op =) head_tfrees (a, S) then I
diff -r b8b672f70d76 -r 1fbad761c1ba src/Pure/theory.ML
--- a/src/Pure/theory.ML	Sun Apr 24 20:29:49 2016 +0200
+++ b/src/Pure/theory.ML	Sun Apr 24 20:37:24 2016 +0200
@@ -291,7 +291,7 @@
 fun check_def (context as (ctxt, _)) thy unchecked overloaded (b, tm) defs =
   let
     val name = Sign.full_name thy b;
-    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (K false) (K false) tm
+    val ((lhs, rhs), _) = Primitive_Defs.dest_def ctxt Term.is_Const (SOME (K false)) (K false) tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);