--- 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) =