# HG changeset patch
# User blanchet
# Date 1392190648 -3600
# Node ID 6445a05a123493740c199ab53e773146c1372d18
# Parent  0aaca907aeab4aae1aeeaf898bf853866872ebfb
compile

diff -r 0aaca907aeab -r 6445a05a1234 src/Doc/Codegen/Refinement.thy
--- a/src/Doc/Codegen/Refinement.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/Doc/Codegen/Refinement.thy	Wed Feb 12 08:37:28 2014 +0100
@@ -148,15 +148,15 @@
   \noindent It is good style, although no absolute requirement, to
   provide code equations for the original artefacts of the implemented
   type, if possible; in our case, these are the datatype constructor
-  @{const Queue} and the case combinator @{const queue_case}:
+  @{const Queue} and the case combinator @{const case_queue}:
 *}
 
 lemma %quote Queue_AQueue [code]:
   "Queue = AQueue []"
   by (simp add: AQueue_def fun_eq_iff)
 
-lemma %quote queue_case_AQueue [code]:
-  "queue_case f (AQueue xs ys) = f (ys @ rev xs)"
+lemma %quote case_queue_AQueue [code]:
+  "case_queue f (AQueue xs ys) = f (ys @ rev xs)"
   by (simp add: AQueue_def)
 
 text {*
@@ -164,7 +164,7 @@
 *}
 
 text %quotetypewriter {*
-  @{code_stmts empty enqueue dequeue Queue queue_case (SML)}
+  @{code_stmts empty enqueue dequeue Queue case_queue (SML)}
 *}
 
 text {*
@@ -274,4 +274,3 @@
 *}
 
 end
-
diff -r 0aaca907aeab -r 6445a05a1234 src/HOL/Decision_Procs/Cooper.thy
--- a/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Cooper.thy	Wed Feb 12 08:37:28 2014 +0100
@@ -303,12 +303,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 x1", auto)
+  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", 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 x1", auto)
+  using nb by (induct xs) (auto simp add: evaldjf_def djf_def Let_def, case_tac "f a", auto)
 
 fun disjuncts :: "fm \<Rightarrow> fm list"
 where
diff -r 0aaca907aeab -r 6445a05a1234 src/HOL/Decision_Procs/Ferrack.thy
--- a/src/HOL/Decision_Procs/Ferrack.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Ferrack.thy	Wed Feb 12 08:37:28 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 x1", auto) 
+  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", 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 x1", auto) 
+  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
 
 fun disjuncts :: "fm \<Rightarrow> fm list" where
   "disjuncts (Or p q) = disjuncts p @ disjuncts q"
@@ -2030,4 +2030,3 @@
   by rferrack
 
 end
-
diff -r 0aaca907aeab -r 6445a05a1234 src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy
--- a/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 2014 +0100
+++ b/src/HOL/Decision_Procs/Parametric_Ferrante_Rackoff.thy	Wed Feb 12 08:37:28 2014 +0100
@@ -761,12 +761,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 x1", auto) 
+  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", 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 x1", auto) 
+  using nb by (induct xs, auto simp add: evaldjf_def djf_def Let_def) (case_tac "f a", auto) 
 
 fun disjuncts :: "fm \<Rightarrow> fm list" where
   "disjuncts (Or p q) = (disjuncts p) @ (disjuncts q)"