--- a/src/HOL/Tools/function_package/context_tree.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/context_tree.ML Tue Jun 06 08:21:14 2006 +0200
@@ -82,7 +82,6 @@
-exception CTREE_INTERNAL of string
fun find_cong_rule thy ((r,dep)::rs) t =
(let
@@ -95,7 +94,7 @@
(r, dep, branches)
end
handle Pattern.MATCH => find_cong_rule thy rs t)
- | find_cong_rule thy [] _ = raise CTREE_INTERNAL "No cong rule found!" (* Should never happen *)
+ | find_cong_rule thy [] _ = sys_error "function_package/context_tree.ML: No cong rule found!"
fun matchcall f (a $ b) = if a = f then SOME b else NONE
--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Jun 06 08:21:14 2006 +0200
@@ -40,17 +40,17 @@
datatype rec_call_info =
- RCInfo
- of {
- RI: thm,
- RIvs: (string * typ) list,
- lRI: thm,
- lRIq: thm,
- Gh: thm,
- Gh': thm,
- GmAs: term list,
- rcarg: term
-}
+ RCInfo of
+ {
+ RI: thm,
+ RIvs: (string * typ) list,
+ lRI: thm,
+ lRIq: thm,
+ Gh: thm,
+ Gh': thm,
+ GmAs: term list,
+ rcarg: term
+ }
datatype clause_info =
ClauseInfo of
@@ -80,10 +80,6 @@
case_hyp: thm
}
-
-datatype curry_info =
- Curry of { argTs: typ list, curry_ss: simpset }
-
type inj_proj = ((term -> term) * (term -> term))
type qgar = (string * typ) list * term list * term list * term
--- a/src/HOL/Tools/function_package/fundef_prep.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_prep.ML Tue Jun 06 08:21:14 2006 +0200
@@ -46,29 +46,6 @@
end
-fun analyze_eqs eqs =
- let
- fun dest_geq geq =
- let
- val qs = add_term_frees (geq, [])
- in
- case dest_implies_list geq of
- (gs, Const ("Trueprop", _) $ (Const ("op =", _) $ (f $ lhs) $ rhs)) =>
- (f, (qs, gs, lhs, rhs))
- | _ => raise ERROR "Not a guarded equation"
- end
-
- val (fs, glrs) = split_list (map dest_geq eqs)
-
- val f = (hd fs) (* should be equal and a constant... check! *)
-
- val used = fold (curry add_term_names) eqs [] (* all names in the eqs *)
- (* Must check for recursive calls in guards and new vars in rhss *)
- in
- (f, glrs, used)
- end
-
-
(* maps (qs,gs,lhs,ths) to (qs',gs',lhs',rhs') with primed variables *)
fun mk_primed_vars thy glrs =
let
@@ -162,8 +139,8 @@
val trees = map (build_tree thy f congs) glrs
val allused = fold FundefCtxTree.add_context_varnames trees used
- val Const (f_proper_name, fT) = f
- val fxname = Sign.extern_const thy f_proper_name
+ val Const (f_fullname, fT) = f
+ val fname = Sign.base_name f_fullname
val domT = domain_type fT
val ranT = range_type fT
@@ -188,15 +165,15 @@
val thy = Sign.add_consts_i [(G_name, GT, NoSyn), (R_name, RT, NoSyn)] thy
- val G = Const (Sign.intern_const thy G_name, GT)
- val R = Const (Sign.intern_const thy R_name, RT)
+ val G = Const (Sign.full_name thy G_name, GT)
+ val R = Const (Sign.full_name thy R_name, RT)
val acc_R = Const (acc_const_name, (fastype_of R) --> HOLogic.mk_setT domT) $ R
val f_eq = Logic.mk_equals (f $ x,
Const ("The", (ranT --> boolT) --> ranT) $
Abs ("y", ranT, mk_relmemT domT ranT (x, Bound 0) G))
- val ([f_def], thy) = PureThy.add_defs_i false [((fxname ^ "_def", f_eq), [])] thy
+ val ([f_def], thy) = PureThy.add_defs_i false [((fname ^ "_def", f_eq), [])] thy
in
(Names {f=f, glrs=glrs, glrs'=glrs', fvar=fvar, fvarname=fvarname, domT=domT, ranT=ranT, G=G, R=R, acc_R=acc_R, h=h, x=x, y=y, z=z, a=a, D=D, P=P, Pbool=Pbool, f_def=f_def, used=allused, trees=trees}, thy)
end
@@ -262,7 +239,7 @@
fun extract_conditions thy names trees congs =
let
- val Names {f, G, R, acc_R, domT, ranT, f_def, x, z, fvarname, glrs, glrs', ...} = names
+ val Names {f, R, glrs, glrs', ...} = names
val (vRiss, preRiss, Riss) = split_list3 (map2 (extract_Ris thy congs f R) trees glrs)
val Gis = map2 (mk_GIntro thy names) glrs preRiss
--- a/src/HOL/Tools/function_package/fundef_proof.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/fundef_proof.ML Tue Jun 06 08:21:14 2006 +0200
@@ -350,9 +350,9 @@
val goal = cterm_of thy (HOLogic.mk_Trueprop (HOLogic.mk_mem (lhs,acc_R)))
in
Goal.init goal
- |> (SINGLE (resolve_tac [accI] 1)) |> print |> the
- |> (SINGLE (eresolve_tac [R_cases] 1)) |> print |> the
- |> (SINGLE (CLASIMPSET auto_tac)) |> print |> the
+ |> (SINGLE (resolve_tac [accI] 1)) |> the
+ |> (SINGLE (eresolve_tac [R_cases] 1)) |> the
+ |> (SINGLE (CLASIMPSET auto_tac)) |> the
|> Goal.conclude
end
--- a/src/HOL/Tools/function_package/mutual.ML Mon Jun 05 21:54:26 2006 +0200
+++ b/src/HOL/Tools/function_package/mutual.ML Tue Jun 06 08:21:14 2006 +0200
@@ -83,11 +83,11 @@
val sfun_type = ST --> RST
val thy = Sign.add_consts_i [(sfun_xname, sfun_type, NoSyn)] thy (* Add the sum function *)
- val sfun = Const (Sign.intern_const thy sfun_xname, sfun_type)
+ val sfun = Const (Sign.full_name thy sfun_xname, sfun_type)
fun define (((((n, T), _), caTs), (pthA, pthR)), qgars) (thy, rews) =
let
- val fxname = Sign.extern_const thy n
+ val fxname = Sign.base_name n
val f = Const (n, T)
val vars = map_index (fn (i,T) => Free ("x" ^ string_of_int i, T)) caTs
@@ -100,9 +100,6 @@
(MutualPart {f_name=fxname, const=(n, T),cargTs=caTs,pthA=pthA,pthR=pthR,qgars=qgars,f_def=f_def}, (thy, rews'))
end
- val _ = print pthsA
- val _ = print pthsR
-
val (parts, (thy, rews)) = fold_map define (((consts ~~ caTss)~~ (pthsA ~~ pthsR)) ~~ qgarss) (thy, [])
fun mk_qglrss (MutualPart {qgars, pthA, pthR, ...}) =