src/HOL/Tools/Function/function_core.ML

                           |> implies_intr (cprop_of complete)
     in
       (goalstate, values)
     end
 
+(* wrapper -- restores quantifiers in rule specifications *)
+fun inductive_def (binding as ((R, T), _)) intrs lthy =
+  let
+    val ({intrs = intrs_gen, elims = [elim_gen], preds = [ Rdef ], induct, ...}, lthy) =
+      lthy
+      |> LocalTheory.conceal
+      |> Inductive.add_inductive_i
+          {quiet_mode = false,
+            verbose = ! Toplevel.debug,
+            kind = Thm.internalK,
+            alt_name = Binding.empty,
+            coind = false,
+            no_elim = false,
+            no_ind = false,
+            skip_mono = true,
+            fork_mono = false}
+          [binding] (* relation *)
+          [] (* no parameters *)
+          (map (fn t => (Attrib.empty_binding, t)) intrs) (* intro rules *)
+          [] (* no special monos *)
+      ||> LocalTheory.restore_naming lthy
+
+    val cert = cterm_of (ProofContext.theory_of lthy)
+    fun requantify orig_intro thm =
+      let
+        val (qs, t) = dest_all_all orig_intro
+        val frees = frees_in_term lthy t |> remove (op =) (Binding.name_of R, T)
+        val vars = Term.add_vars (prop_of thm) [] |> rev
+        val varmap = AList.lookup (op =) (frees ~~ map fst vars)
+          #> the_default ("",0)
+      in
+        fold_rev (fn Free (n, T) =>
+          forall_intr_rename (n, cert (Var (varmap (n, T), T)))) qs thm
+      end
+  in
+      ((map2 requantify intrs intrs_gen, Rdef, forall_intr_vars elim_gen, induct), lthy)
+  end
+
 
 fun define_graph Gname fvar domT ranT clauses RCss lthy =
     let
       val GT = domT --> ranT --> boolT
-      val Gvar = Free (the_single (Variable.variant_frees lthy [] [(Gname, GT)]))
+      val (Gvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Gname, GT)])
 
       fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
           let
             fun mk_h_assm (rcfix, rcassm, rcarg) =
-                HOLogic.mk_Trueprop (Gvar $ rcarg $ (fvar $ rcarg))
+                HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
                           |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                           |> fold_rev (Logic.all o Free) rcfix
           in
-            HOLogic.mk_Trueprop (Gvar $ lhs $ rhs)
+            HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
                       |> fold_rev (curry Logic.mk_implies o mk_h_assm) RCs
                       |> fold_rev (curry Logic.mk_implies) gs
                       |> fold_rev Logic.all (fvar :: qs)
           end
 
       val G_intros = map2 mk_GIntro clauses RCss
 
-      val (GIntro_thms, (G, G_elim, G_induct, lthy)) =
-          Function_Inductive_Wrap.inductive_def G_intros ((dest_Free Gvar, NoSyn), lthy)
+      val ((GIntro_thms, G, G_elim, G_induct), lthy) =
+        inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
     in
       ((G, GIntro_thms, G_elim, G_induct), lthy)
     end
 
 

 
 fun define_recursion_relation Rname domT ranT fvar f qglrs clauses RCss lthy =
     let
 
       val RT = domT --> domT --> boolT
-      val Rvar = Free (the_single (Variable.variant_frees lthy [] [(Rname, RT)]))
+      val (Rvar as (n, T)) = the_single (Variable.variant_frees lthy [] [(Rname, RT)])
 
       fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-          HOLogic.mk_Trueprop (Rvar $ rcarg $ lhs)
+          HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
                     |> fold_rev (curry Logic.mk_implies o prop_of) rcassm
                     |> fold_rev (curry Logic.mk_implies) gs
                     |> fold_rev (Logic.all o Free) rcfix
                     |> fold_rev mk_forall_rename (map fst oqs ~~ qs)
                     (* "!!qs xs. CS ==> G => (r, lhs) : R" *)
 
       val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
-      val (RIntro_thmss, (R, R_elim, _, lthy)) =
-          fold_burrow Function_Inductive_Wrap.inductive_def R_intross ((dest_Free Rvar, NoSyn), lthy)
-    in
-      ((R, RIntro_thmss, R_elim), lthy)
+      val ((RIntro_thms, R, R_elim, _), lthy) =
+        inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+    in
+      ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
     end
 
 
 fun fix_globals domT ranT fvar ctxt =
     let