src/Pure/primitive_defs.ML

 Primitive definition forms.
 *)
 
 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;
 
 structure Primitive_Defs: PRIMITIVE_DEFS =

   | term_kind (Free _) = "free variable "
   | term_kind (Bound _) = "bound variable "
   | 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;
     val eq_body = Term.strip_all_body eq;
 

     val lhs = Envir.beta_eta_contract raw_lhs;
     val (head, args) = Term.strip_comb lhs;
     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
       | close_arg x t = Logic.all x t;
 
     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
       err ("Bad head of lhs: " ^ term_kind head ^ display_terms [head])
     else if not (null lhs_bads) then