avoid hardwired frees;
tuned;

--- a/src/HOL/Tools/Function/function_core.ML	Tue Oct 06 16:57:14 2015 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Tue Oct 06 17:31:42 2015 +0200
@@ -86,10 +86,6 @@
 
 val acc_downward = @{thm accp_downward}
 val accI = @{thm accp.accI}
-val case_split = @{thm HOL.case_split}
-val fundef_default_value = @{thm Fun_Def.fundef_default_value}
-val not_acc_down = @{thm not_accp_down}
-
 
 
 fun find_calls tree =
@@ -259,8 +255,7 @@
 (* Generates the replacement lemma in fully quantified form. *)
 fun mk_replacement_lemma ctxt h ih_elim clause =
   let
-    val ClauseInfo {cdata=ClauseContext {qs, lhs, cqs, ags, case_hyp, ...},
-      RCs, tree, ...} = clause
+    val ClauseInfo {cdata=ClauseContext {qs, cqs, ags, case_hyp, ...}, RCs, tree, ...} = clause
     local open Conv in
       val ih_conv = arg1_conv o arg_conv o arg_conv
     end
@@ -784,50 +779,51 @@
     val Globals { domT, x, z, ... } = globals
     val acc_R = mk_acc domT R
 
-    val R' = Free ("R", fastype_of R)
+    val ([Rn], ctxt') = Variable.variant_fixes ["R"] ctxt
+    val R' = Free (Rn, fastype_of R)
 
-    val Rrel = Free ("R", HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
+    val Rrel = Free (Rn, HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)))
     val inrel_R = Const (@{const_name Fun_Def.in_rel},
       HOLogic.mk_setT (HOLogic.mk_prodT (domT, domT)) --> fastype_of R) $ Rrel
 
     val wfR' = HOLogic.mk_Trueprop (Const (@{const_name Wellfounded.wfP},
       (domT --> domT --> boolT) --> boolT) $ R')
-      |> Thm.cterm_of ctxt (* "wf R'" *)
+      |> Thm.cterm_of ctxt' (* "wf R'" *)
 
     (* Inductive Hypothesis: !!z. (z,x):R' ==> z : acc R *)
     val ihyp = Logic.all_const domT $ Abs ("z", domT,
       Logic.mk_implies (HOLogic.mk_Trueprop (R' $ Bound 0 $ x),
         HOLogic.mk_Trueprop (acc_R $ Bound 0)))
-      |> Thm.cterm_of ctxt
+      |> Thm.cterm_of ctxt'
 
     val ihyp_a = Thm.assume ihyp |> Thm.forall_elim_vars 0
 
-    val R_z_x = Thm.cterm_of ctxt (HOLogic.mk_Trueprop (R $ z $ x))
+    val R_z_x = Thm.cterm_of ctxt' (HOLogic.mk_Trueprop (R $ z $ x))
 
-    val (hyps, cases) = fold (mk_nest_term_case ctxt globals R' ihyp_a) clauses ([], [])
+    val (hyps, cases) = fold (mk_nest_term_case ctxt' globals R' ihyp_a) clauses ([], [])
   in
     R_cases
-    |> Thm.forall_elim (Thm.cterm_of ctxt z)
-    |> Thm.forall_elim (Thm.cterm_of ctxt x)
-    |> Thm.forall_elim (Thm.cterm_of ctxt (acc_R $ z))
+    |> Thm.forall_elim (Thm.cterm_of ctxt' z)
+    |> Thm.forall_elim (Thm.cterm_of ctxt' x)
+    |> Thm.forall_elim (Thm.cterm_of ctxt' (acc_R $ z))
     |> curry op COMP (Thm.assume R_z_x)
     |> fold_rev (curry op COMP) cases
     |> Thm.implies_intr R_z_x
-    |> Thm.forall_intr (Thm.cterm_of ctxt z)
+    |> Thm.forall_intr (Thm.cterm_of ctxt' z)
     |> (fn it => it COMP accI)
     |> Thm.implies_intr ihyp
-    |> Thm.forall_intr (Thm.cterm_of ctxt x)
+    |> Thm.forall_intr (Thm.cterm_of ctxt' x)
     |> (fn it => Drule.compose (it, 2, wf_induct_rule))
     |> curry op RS (Thm.assume wfR')
     |> forall_intr_vars
     |> (fn it => it COMP allI)
     |> fold Thm.implies_intr hyps
     |> Thm.implies_intr wfR'
-    |> Thm.forall_intr (Thm.cterm_of ctxt R')
-    |> Thm.forall_elim (Thm.cterm_of ctxt (inrel_R))
+    |> Thm.forall_intr (Thm.cterm_of ctxt' R')
+    |> Thm.forall_elim (Thm.cterm_of ctxt' inrel_R)
     |> curry op RS wf_in_rel
-    |> full_simplify (put_simpset HOL_basic_ss ctxt addsimps [in_rel_def])
-    |> Thm.forall_intr (Thm.cterm_of ctxt Rrel)
+    |> full_simplify (put_simpset HOL_basic_ss ctxt' addsimps [in_rel_def])
+    |> Thm.forall_intr_name ("R", Thm.cterm_of ctxt' Rrel)
   end
 
 

--- a/src/HOL/Tools/Function/induction_schema.ML	Tue Oct 06 16:57:14 2015 +0200
+++ b/src/HOL/Tools/Function/induction_schema.ML	Tue Oct 06 17:31:42 2015 +0200
@@ -142,12 +142,12 @@
 fun mk_wf R (IndScheme {T, ...}) =
   HOLogic.Trueprop $ (Const (@{const_name wf}, mk_relT T --> HOLogic.boolT) $ R)
 
-fun mk_ineqs R (IndScheme {T, cases, branches}) =
+fun mk_ineqs R thesisn (IndScheme {T, cases, branches}) =
   let
     fun inject i ts =
        Sum_Tree.mk_inj T (length branches) (i + 1) (foldr1 HOLogic.mk_prod ts)
 
-    val thesis = Free ("thesis", HOLogic.boolT) (* FIXME *)
+    val thesis = Free (thesisn, HOLogic.boolT)
 
     fun mk_pres bdx args =
       let
@@ -349,12 +349,12 @@
   let
     val (ctxt', _, cases, concl) = dest_hhf ctxt t
     val scheme as IndScheme {T=ST, branches, ...} = mk_scheme' ctxt' cases concl
-    val ([Rn, xn], ctxt'') = Variable.variant_fixes ["R", "x"] ctxt'
+    val ([Rn, xn, thesisn], ctxt'') = Variable.variant_fixes ["R", "x", "thesis"] ctxt'
     val R = Free (Rn, mk_relT ST)
     val x = Free (xn, ST)
 
     val ineqss =
-      mk_ineqs R scheme
+      mk_ineqs R thesisn scheme
       |> map (map (apply2 (Thm.assume o Thm.cterm_of ctxt'')))
     val complete =
       map_range (mk_completeness ctxt'' scheme #> Thm.cterm_of ctxt'' #> Thm.assume)