src/Pure/primitive_defs.ML

--- a/src/Pure/primitive_defs.ML	Tue Jul 05 10:32:25 2016 +0200
+++ b/src/Pure/primitive_defs.ML	Tue Jul 05 14:20:27 2016 +0200
@@ -11,7 +11,7 @@
      check_free_lhs: string -> bool,
      check_free_rhs: string -> bool,
      check_tfree: string -> bool} ->
-    term -> (term * term) * term
+    term -> (term * term) * term list * term
   val abs_def: term -> term * term
 end;
 
@@ -68,7 +68,8 @@
     else if exists_subterm (fn t => t aconv head) rhs then
       err "Entity to be defined occurs on rhs"
     else
-      ((lhs, rhs), fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
+      ((lhs, rhs), args,
+        fold_rev close_arg args (Logic.list_all (eq_vars, (Logic.mk_equals (lhs, rhs)))))
   end;
 
 (*!!x. c x == t[x] to c == %x. t[x]*)