--- a/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:35:57 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy Wed Feb 12 08:37:06 2014 +0100
@@ -328,12 +328,12 @@
lemma evaldjf_bound0:
assumes nb: "\<forall> x\<in> set xs. bound0 (f x)"
shows "bound0 (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
lemma evaldjf_qf:
assumes nb: "\<forall> x\<in> set xs. qfree (f x)"
shows "qfree (evaldjf f xs)"
- using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto)
+ using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f x1", auto)
fun disjuncts :: "fm \<Rightarrow> fm list" where
"disjuncts (Or p q) = disjuncts p @ disjuncts q"