# HG changeset patch
# User wenzelm
# Date 1461598656 -7200
# Node ID 741263be960ee68d43e85aa7d008c707374ad3ab
# Parent  cb495c4807b31cd1011da6ec9a0aeac95d6d8477
more rigid check of lhs;

diff -r cb495c4807b3 -r 741263be960e src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Mon Apr 25 16:54:48 2016 +0200
+++ b/src/Pure/Isar/local_defs.ML	Mon Apr 25 17:37:36 2016 +0200
@@ -44,10 +44,13 @@
     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 is_fixed (K true)
+      |> Primitive_Defs.dest_def ctxt
+        {check_head = Term.is_Free,
+         check_free_lhs = not o Variable.is_fixed ctxt,
+         check_free_rhs = if Variable.is_body ctxt then K true else Variable.is_fixed ctxt,
+         check_tfree = K true}
       handle TERM (msg, _) => err msg | ERROR msg => err msg;
   in (Term.dest_Free (Term.head_of lhs), eq') end;
 
diff -r cb495c4807b3 -r 741263be960e src/Pure/primitive_defs.ML
--- a/src/Pure/primitive_defs.ML	Mon Apr 25 16:54:48 2016 +0200
+++ b/src/Pure/primitive_defs.ML	Mon Apr 25 17:37:36 2016 +0200
@@ -6,7 +6,11 @@
 
 signature PRIMITIVE_DEFS =
 sig
-  val dest_def: Proof.context -> (term -> bool) -> (string -> bool) option -> (string -> bool) ->
+  val dest_def: Proof.context ->
+    {check_head: term -> bool,
+     check_free_lhs: string -> bool,
+     check_free_rhs: string -> bool,
+     check_tfree: string -> bool} ->
     term -> (term * term) * term
   val abs_def: term -> term * term
 end;
@@ -20,7 +24,7 @@
   | term_kind _ = "";
 
 (*c x == t[x] to !!x. c x == t[x]*)
-fun dest_def ctxt check_head is_fixed is_fixedT eq =
+fun dest_def ctxt {check_head, check_free_lhs, check_free_rhs, check_tfree} eq =
   let
     fun err msg = raise TERM (msg, [eq]);
     val eq_vars = Term.strip_all_vars eq;
@@ -36,7 +40,7 @@
     val head_tfrees = Term.add_tfrees head [];
 
     fun check_arg (Bound _) = true
-      | check_arg (Free (x, _)) = is_none is_fixed orelse not (the is_fixed x)
+      | check_arg (Free (x, _)) = check_free_lhs x
       | check_arg (Const ("Pure.type", Type ("itself", [TFree _]))) = true
       | check_arg _ = false;
     fun close_arg (Bound _) t = t
@@ -45,10 +49,10 @@
     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_none is_fixed orelse the is_fixed x orelse member (op aconv) args v then I
+      if check_free_rhs 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
+      if check_tfree a orelse member (op =) head_tfrees (a, S) then I
       else insert (op =) v | _ => I)) rhs [];
   in
     if not (check_head head) then
diff -r cb495c4807b3 -r 741263be960e src/Pure/theory.ML
--- a/src/Pure/theory.ML	Mon Apr 25 16:54:48 2016 +0200
+++ b/src/Pure/theory.ML	Mon Apr 25 17:37:36 2016 +0200
@@ -291,7 +291,12 @@
 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 (SOME (K false)) (K false) tm
+    val ((lhs, rhs), _) =
+      Primitive_Defs.dest_def ctxt
+        {check_head = Term.is_Const,
+         check_free_lhs = K true,
+         check_free_rhs = K false,
+         check_tfree = K false} tm
       handle TERM (msg, _) => error msg;
     val lhs_const = Term.dest_Const (Term.head_of lhs);