# HG changeset patch # User lcp # Date 758905060 -3600 # Node ID ec8a2b6aa8a7ee30e00544a66c7c373b6506a05f # Parent 4002c4cd450c0e579b53956b21ae7bf57a50bc61 Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g diff -r 4002c4cd450c -r ec8a2b6aa8a7 src/Pure/goals.ML --- a/src/Pure/goals.ML Tue Jan 18 13:46:08 1994 +0100 +++ b/src/Pure/goals.ML Tue Jan 18 15:57:40 1994 +0100 @@ -41,7 +41,7 @@ val gethyps: int -> thm list val goal: theory -> string -> thm list val goalw: theory -> thm list -> string -> thm list - val goalw_cterm: thm list -> Sign.cterm -> thm list + val goalw_cterm: thm list -> cterm -> thm list val pop_proof: unit -> thm list val pr: unit -> unit val premises: unit -> thm list @@ -54,7 +54,7 @@ val proof_timing: bool ref val prove_goal: theory -> string -> (thm list -> tactic list) -> thm val prove_goalw: theory->thm list->string->(thm list->tactic list)->thm - val prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm + val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm val push_proof: unit -> unit val read: string -> term val ren: string -> int -> unit @@ -99,7 +99,7 @@ ref((fn _=> error"No goal has been supplied in subgoal module") : bool*thm->thm); -val dummy = trivial(Sign.read_cterm Sign.pure +val dummy = trivial(read_cterm Sign.pure ("PROP No_goal_has_been_supplied",propT)); (*List of previous goal stacks, for the undo operation. Set by setstate. @@ -124,13 +124,13 @@ (*Common treatment of "goal" and "prove_goal": Return assumptions, initial proof state, and function to make result. *) fun prepare_proof rths chorn = - let val {sign, t=horn,...} = Sign.rep_cterm chorn; + let val {sign, t=horn,...} = rep_cterm chorn; val (_,As,B) = Logic.strip_horn(horn); - val cAs = map (Sign.cterm_of sign) As; + val cAs = map (cterm_of sign) As; val p_rew = if null rths then I else rewrite_rule rths; val c_rew = if null rths then I else rewrite_goals_rule rths; val prems = map (p_rew o forall_elim_vars(0) o assume) cAs - and st0 = c_rew (trivial (Sign.cterm_of sign B)) + and st0 = c_rew (trivial (cterm_of sign B)) fun result_error state msg = (writeln ("Bad final proof state:"); !print_goals_ref (!goals_limit) state; @@ -151,7 +151,7 @@ ("Additional hypotheses:\n" ^ cat_lines (map (Sign.string_of_term sign) hyps)) else if Pattern.eta_matches (#tsig(Sign.rep_sg sign)) - (Sign.term_of chorn, prop) + (term_of chorn, prop) then standard th else result_error state "proved a different theorem" end @@ -199,7 +199,7 @@ (*Version taking the goal as a string*) fun prove_goalw thy rths agoal tacsf = let val sign = sign_of thy - val chorn = Sign.read_cterm sign (agoal,propT) + val chorn = read_cterm sign (agoal,propT) in prove_goalw_cterm rths chorn tacsf handle ERROR => error (*from type_assign, etc via prepare_proof*) ("The error above occurred for " ^ quote agoal) @@ -286,7 +286,7 @@ Initial subgoal and premises are rewritten using rths. **) (*Version taking the goal as a cterm; if you have a term t and theory thy, use - goalw_cterm rths (Sign.cterm_of (sign_of thy) t); *) + goalw_cterm rths (cterm_of (sign_of thy) t); *) fun goalw_cterm rths chorn = let val (prems, st0, mkresult) = prepare_proof rths chorn in undo_list := []; @@ -298,7 +298,7 @@ (*Version taking the goal as a string*) fun goalw thy rths agoal = - goalw_cterm rths (Sign.read_cterm(sign_of thy)(agoal,propT)) + goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT)) handle ERROR => error (*from type_assign, etc via prepare_proof*) ("The error above occurred for " ^ quote agoal); @@ -418,7 +418,7 @@ fun top_sg() = #sign(rep_thm(topthm())); -fun read s = Sign.term_of (Sign.read_cterm (top_sg()) +fun read s = term_of (read_cterm (top_sg()) (s, (TVar(("DUMMY",0),[])))); (*Print a term under the current signature of the proof state*) diff -r 4002c4cd450c -r ec8a2b6aa8a7 src/Pure/install_pp.ML --- a/src/Pure/install_pp.ML Tue Jan 18 13:46:08 1994 +0100 +++ b/src/Pure/install_pp.ML Tue Jan 18 15:57:40 1994 +0100 @@ -4,12 +4,12 @@ Set up automatic toplevel printing *) -install_pp (make_pp ["Thm", "thm"] pprint_thm); -install_pp (make_pp ["Thm", "theory"] pprint_theory); -install_pp (make_pp ["Sign", "sg"] pprint_sg); -install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm); -install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp); -install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); +install_pp (make_pp ["Thm", "thm"] pprint_thm); +install_pp (make_pp ["Thm", "theory"] pprint_theory); +install_pp (make_pp ["Thm", "cterm"] pprint_cterm); +install_pp (make_pp ["Thm", "ctyp"] pprint_ctyp); +install_pp (make_pp ["Sign", "sg"] pprint_sg); +install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast); (* install_pp (make_pp ["term"] pprint_term); diff -r 4002c4cd450c -r ec8a2b6aa8a7 src/Pure/tactic.ML --- a/src/Pure/tactic.ML Tue Jan 18 13:46:08 1994 +0100 +++ b/src/Pure/tactic.ML Tue Jan 18 15:57:40 1994 +0100 @@ -99,8 +99,8 @@ let val fth = freezeT th val {prop,sign,...} = rep_thm fth fun mk_inst (Var(v,T)) = - (Sign.cterm_of sign (Var(v,T)), - Sign.cterm_of sign (Free(string_of v, T))) + (cterm_of sign (Var(v,T)), + cterm_of sign (Free(string_of v, T))) val insts = map mk_inst (term_vars prop) in instantiate ([],insts) fth end; @@ -184,14 +184,14 @@ fun liftterm t = list_abs_free (params, Logic.incr_indexes(paramTs,inc) t) (*Lifts instantiation pair over params*) - fun liftpair (cv,ct) = (Sign.cfun liftvar cv, Sign.cfun liftterm ct) + fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) fun lifttvar((a,i),ctyp) = - let val {T,sign} = Sign.rep_ctyp ctyp - in ((a,i+inc), Sign.ctyp_of sign (incr_tvar inc T)) end + let val {T,sign} = rep_ctyp ctyp + in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end val rts = types_sorts rule and (types,sorts) = types_sorts state fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm) | types'(ixn) = types ixn; - val (Tinsts,insts) = Sign.read_insts sign rts (types',sorts) sinsts + val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts in instantiate (map lifttvar Tinsts, map liftpair insts) (lift_rule (state,i) rule) end; diff -r 4002c4cd450c -r ec8a2b6aa8a7 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Tue Jan 18 13:46:08 1994 +0100 +++ b/src/Pure/tctical.ML Tue Jan 18 15:57:40 1994 +0100 @@ -399,7 +399,7 @@ (* (!!x. PROP ?V) ==> PROP ?V ; contains NO TYPE VARIABLES.*) val dummy_quant_rl = standard (forall_elim_var 0 (assume - (Sign.read_cterm Sign.pure ("!!x::prop. PROP V",propT)))); + (read_cterm Sign.pure ("!!x::prop. PROP V",propT)))); (* Prevent the subgoal's assumptions from becoming additional subgoals in the new proof state by enclosing them by a universal quantification *) @@ -411,7 +411,7 @@ (*Does the work of SELECT_GOAL. *) fun select (Tactic tf) state i = let val prem::_ = drop(i-1, prems_of state) - val st0 = trivial (Sign.cterm_of (#sign(rep_thm state)) prem); + val st0 = trivial (cterm_of (#sign(rep_thm state)) prem); fun next st = bicompose false (false, st, nprems_of st) i state in Sequence.flats (Sequence.maps next (tf st0)) end; @@ -469,7 +469,7 @@ fun metahyps_aux_tac tacf (prem,i) = Tactic (fn state => let val {sign,maxidx,...} = rep_thm state - val cterm = Sign.cterm_of sign + val cterm = cterm_of sign (*find all vars in the hyps -- should find tvars also!*) val hyps_vars = foldr add_term_vars (strip_assums_hyp prem, []) val insts = map mk_inst hyps_vars