# HG changeset patch # User wenzelm # Date 1119298460 -7200 # Node ID c4b2e3cd84ab8c312305b729171239788ae3507a # Parent 7c1cb7ce24eb1235098fa502d1c3a19488df5f76 avoid identifier 'Name'; diff -r 7c1cb7ce24eb -r c4b2e3cd84ab TFL/tfl.ML --- a/TFL/tfl.ML Mon Jun 20 22:14:19 2005 +0200 +++ b/TFL/tfl.ML Mon Jun 20 22:14:20 2005 +0200 @@ -101,13 +101,13 @@ | part {constrs = [], rows = _::_, A} = pfail"extra cases in defn" | part {constrs = _::_, rows = [], A} = pfail"cases missing in defn" | part {constrs = c::crst, rows, A} = - let val (Name,Ty) = dest_Const c - val L = binder_types Ty + let val (c, T) = dest_Const c + val L = binder_types T val (in_group, not_in_group) = U.itlist (fn (row as (p::rst, rhs)) => fn (in_group,not_in_group) => let val (pc,args) = S.strip_comb p - in if (#1(dest_Const pc) = Name) + in if (#1(dest_Const pc) = c) then ((args@rst, rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]) @@ -157,13 +157,13 @@ (*--------------------------------------------------------------------------- * Goes through a list of rows and picks out the ones beginning with a - * pattern with constructor = Name. + * pattern with constructor = name. *---------------------------------------------------------------------------*) -fun mk_group Name rows = +fun mk_group name rows = U.itlist (fn (row as ((prfx, p::rst), rhs)) => fn (in_group,not_in_group) => let val (pc,args) = S.strip_comb p - in if ((#1 (Term.dest_Const pc) = Name) handle TERM _ => false) + in if ((#1 (Term.dest_Const pc) = name) handle TERM _ => false) then (((prfx,args@rst), rhs)::in_group, not_in_group) else (in_group, row::not_in_group) end) rows ([],[]); @@ -178,8 +178,7 @@ fun part {constrs = [], rows, A} = rev A | part {constrs = c::crst, rows, A} = let val (c',gvars) = fresh c - val (Name,Ty) = dest_Const c' - val (in_group, not_in_group) = mk_group Name rows + val (in_group, not_in_group) = mk_group (#1 (dest_Const c')) rows val in_group' = if (null in_group) (* Constructor not given *) then [((prfx, #2(fresh c)), (S.ARB res_ty, (~1,false)))] @@ -290,7 +289,7 @@ (* Repeated variable occurrences in a pattern are not allowed. *) fun FV_multiset tm = case (S.dest_term tm) - of S.VAR{Name,Ty} => [Free(Name,Ty)] + of S.VAR{Name = c, Ty = T} => [Free(c, T)] | S.CONST _ => [] | S.COMB{Rator, Rand} => FV_multiset Rator @ FV_multiset Rand | S.LAMB _ => raise TFL_ERR "FV_multiset" "lambda"; @@ -370,9 +369,9 @@ (*For Isabelle, the lhs of a definition must be a constant.*) -fun mk_const_def sign (Name, Ty, rhs) = +fun mk_const_def sign (c, Ty, rhs) = Sign.infer_types (Sign.pp sign) sign (K NONE) (K NONE) [] false - ([Const("==",dummyT) $ Const(Name,Ty) $ rhs], propT) + ([Const("==",dummyT) $ Const(c,Ty) $ rhs], propT) |> #1; (*Make all TVars available for instantiation by adding a ? to the front*) @@ -386,17 +385,17 @@ val (fname,_) = dest_Free f val (wfrec,_) = S.strip_comb rhs in -fun wfrec_definition0 thy fid R (functional as Abs(Name, Ty, _)) = - let val def_name = if Name<>fid then +fun wfrec_definition0 thy fid R (functional as Abs(x, Ty, _)) = + let val def_name = if x<>fid then raise TFL_ERR "wfrec_definition0" ("Expected a definition of " ^ quote fid ^ " but found one of " ^ - quote Name) - else Name ^ "_def" + quote x) + else x ^ "_def" val wfrec_R_M = map_term_types poly_tvars (wfrec $ map_term_types poly_tvars R) $ functional - val def_term = mk_const_def (Theory.sign_of thy) (Name, Ty, wfrec_R_M) + val def_term = mk_const_def (Theory.sign_of thy) (x, Ty, wfrec_R_M) val (thy', [def]) = PureThy.add_defs_i false [Thm.no_attributes (def_name, def_term)] thy in (thy', def) end; end; @@ -449,7 +448,7 @@ given_pats val (case_rewrites,context_congs) = extraction_thms theory (*case_ss causes minimal simplification: bodies of case expressions are - not simplified. Otherwise large examples (Red-Black trees) are too + not simplified. Otherwise large examples (Red-Black trees) are too slow.*) val case_ss = HOL_basic_ss addcongs DatatypePackage.weak_case_congs_of theory addsimps case_rewrites @@ -485,15 +484,15 @@ val g = list_comb(f,SV) val h = Free(fname,type_of g) val eqns1 = map (subst_free[(g,h)]) eqns - val {functional as Abs(Name, Ty, _), pats} = mk_functional thy eqns1 + val {functional as Abs(x, Ty, _), pats} = mk_functional thy eqns1 val given_pats = givens pats - (* val f = Free(Name,Ty) *) + (* val f = Free(x,Ty) *) val Type("fun", [f_dty, f_rty]) = Ty - val dummy = if Name<>fid then + val dummy = if x<>fid then raise TFL_ERR "wfrec_eqns" ("Expected a definition of " ^ quote fid ^ " but found one of " ^ - quote Name) + quote x) else () val (case_rewrites,context_congs) = extraction_thms thy val tych = Thry.typecheck thy @@ -551,9 +550,9 @@ else () val {lhs,rhs} = S.dest_eq proto_def' val (c,args) = S.strip_comb lhs - val (Name,Ty) = dest_atom c + val (name,Ty) = dest_atom c val defn = mk_const_def (Theory.sign_of thy) - (Name, Ty, S.list_mk_abs (args,rhs)) + (name, Ty, S.list_mk_abs (args,rhs)) val (theory, [def0]) = thy |> PureThy.add_defs_i false @@ -580,7 +579,7 @@ val body_th = R.LIST_CONJ (map R.ASSUME full_rqt_prop) val SELECT_AX = (*in this way we hope to avoid a STATIC dependence upon theory Hilbert_Choice*) - thm "Hilbert_Choice.tfl_some" + thm "Hilbert_Choice.tfl_some" handle ERROR => error "defer_recdef requires theory Main or at least Hilbert_Choice as parent" val bar = R.MP (R.ISPECL[tych R'abs, tych R1] SELECT_AX) body_th