# HG changeset patch
# User wenzelm
# Date 1460903315 -7200
# Node ID 637ed69b4d46c19a633e4d7a70aa35476a86da71
# Parent  d0dfdd413a7f6a9f281574029cea29353406d8c5
prefer precise names for internal construction;

diff -r d0dfdd413a7f -r 637ed69b4d46 src/HOL/Tools/Function/function_core.ML
--- a/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 16:02:44 2016 +0200
+++ b/src/HOL/Tools/Function/function_core.ML	Sun Apr 17 16:28:35 2016 +0200
@@ -469,19 +469,17 @@
     ((Rdef, map2 requantify intrs intrs_gen, forall_intr_vars elim_gen, induct), lthy)
   end
 
-fun define_graph Gname fvar domT ranT clauses RCss lthy =
+fun define_graph (G_name, G_type) fvar clauses RCss lthy =
   let
-    val GT = domT --> ranT --> boolT
-    val (Gvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Gname, GT)
-
+    val G = Free (G_name, G_type)
     fun mk_GIntro (ClauseContext {qs, gs, lhs, rhs, ...}) RCs =
       let
         fun mk_h_assm (rcfix, rcassm, rcarg) =
-          HOLogic.mk_Trueprop (Free Gvar $ rcarg $ (fvar $ rcarg))
+          HOLogic.mk_Trueprop (G $ rcarg $ (fvar $ rcarg))
           |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
           |> fold_rev (Logic.all o Free) rcfix
       in
-        HOLogic.mk_Trueprop (Free Gvar $ lhs $ rhs)
+        HOLogic.mk_Trueprop (G $ 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)
@@ -489,7 +487,7 @@
 
     val G_intros = map2 mk_GIntro clauses RCss
   in
-    inductive_def ((Binding.name n, T), NoSyn) G_intros lthy
+    inductive_def ((Binding.name G_name, G_type), NoSyn) G_intros lthy
   end
 
 fun define_function fdefname (fname, mixfix) domT ranT G default lthy =
@@ -506,13 +504,10 @@
       ((Binding.name (function_name fname), mixfix), (def_binding, f_def)) lthy
   end
 
-fun define_recursion_relation Rname domT qglrs clauses RCss lthy =
+fun define_recursion_relation (R_name, R_type) qglrs clauses RCss lthy =
   let
-    val RT = domT --> domT --> boolT
-    val (Rvar as (n, T)) = singleton (Variable.variant_frees lthy []) (Rname, RT)
-
     fun mk_RIntro (ClauseContext {qs, gs, lhs, ...}, (oqs, _, _, _)) (rcfix, rcassm, rcarg) =
-      HOLogic.mk_Trueprop (Free Rvar $ rcarg $ lhs)
+      HOLogic.mk_Trueprop (Free (R_name, R_type) $ rcarg $ lhs)
       |> fold_rev (curry Logic.mk_implies o Thm.prop_of) rcassm
       |> fold_rev (curry Logic.mk_implies) gs
       |> fold_rev (Logic.all o Free) rcfix
@@ -522,7 +517,7 @@
     val R_intross = map2 (map o mk_RIntro) (clauses ~~ qglrs) RCss
 
     val ((R, RIntro_thms, R_elim, _), lthy) =
-      inductive_def ((Binding.name n, T), NoSyn) (flat R_intross) lthy
+      inductive_def ((Binding.name R_name, R_type), NoSyn) (flat R_intross) lthy
   in
     ((R, Library.unflat R_intross RIntro_thms, R_elim), lthy)
   end
@@ -855,7 +850,8 @@
     val RCss = map find_calls trees
 
     val ((G, GIntro_thms, G_elim, G_induct), lthy) =
-      PROFILE "def_graph" (define_graph (graph_name defname) fvar domT ranT clauses RCss) lthy
+      PROFILE "def_graph"
+        (define_graph (graph_name defname, domT --> ranT --> boolT) fvar clauses RCss) lthy
 
     val ((f, (_, f_defthm)), lthy) =
       PROFILE "def_fun" (define_function (defname ^ "_sumC_def") (fname, mixfix) domT ranT G default) lthy
@@ -864,7 +860,9 @@
     val trees = map (Function_Context_Tree.inst_tree lthy fvar f) trees
 
     val ((R, RIntro_thmss, R_elim), lthy) =
-      PROFILE "def_rel" (define_recursion_relation (rel_name defname) domT abstract_qglrs clauses RCss) lthy
+      PROFILE "def_rel"
+        (define_recursion_relation (rel_name defname, domT --> domT --> boolT)
+          abstract_qglrs clauses RCss) lthy
 
     val dom = mk_acc domT R
     val (_, lthy) =