--- a/src/HOL/Tools/inductive_set.ML Thu Apr 07 22:09:23 2016 +0200
+++ b/src/HOL/Tools/inductive_set.ML Fri Apr 08 20:15:20 2016 +0200
@@ -98,8 +98,7 @@
end
else NONE
| _ => NONE)
- end,
- identifier = []};
+ end};
(* only eta contract terms occurring as arguments of functions satisfying p *)
fun eta_contract p =
@@ -319,8 +318,7 @@
{lhss = [anyt],
proc = fn _ => fn ctxt => fn ct =>
lookup_rule (Proof_Context.theory_of ctxt)
- (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct),
- identifier = []}
+ (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)}
end;
fun to_pred_proc thy rules t =