Many other files modified as follows:
authorlcp
Tue Jan 18 15:57:40 1994 +0100 (1994-01-18)
changeset 230ec8a2b6aa8a7
parent 229 4002c4cd450c
child 231 cb6a24451544
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
src/Pure/goals.ML
src/Pure/install_pp.ML
src/Pure/tactic.ML
src/Pure/tctical.ML
     1.1 --- a/src/Pure/goals.ML	Tue Jan 18 13:46:08 1994 +0100
     1.2 +++ b/src/Pure/goals.ML	Tue Jan 18 15:57:40 1994 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4    val gethyps: int -> thm list
     1.5    val goal:  theory -> string -> thm list
     1.6    val goalw: theory -> thm list -> string -> thm list
     1.7 -  val goalw_cterm:     thm list -> Sign.cterm -> thm list
     1.8 +  val goalw_cterm:     thm list -> cterm -> thm list
     1.9    val pop_proof: unit -> thm list
    1.10    val pr: unit -> unit
    1.11    val premises: unit -> thm list
    1.12 @@ -54,7 +54,7 @@
    1.13    val proof_timing: bool ref
    1.14    val prove_goal: theory -> string -> (thm list -> tactic list) -> thm
    1.15    val prove_goalw: theory->thm list->string->(thm list->tactic list)->thm
    1.16 -  val prove_goalw_cterm: thm list->Sign.cterm->(thm list->tactic list)->thm
    1.17 +  val prove_goalw_cterm: thm list->cterm->(thm list->tactic list)->thm
    1.18    val push_proof: unit -> unit
    1.19    val read: string -> term
    1.20    val ren: string -> int -> unit
    1.21 @@ -99,7 +99,7 @@
    1.22      ref((fn _=> error"No goal has been supplied in subgoal module") 
    1.23         : bool*thm->thm);
    1.24  
    1.25 -val dummy = trivial(Sign.read_cterm Sign.pure 
    1.26 +val dummy = trivial(read_cterm Sign.pure 
    1.27      ("PROP No_goal_has_been_supplied",propT));
    1.28  
    1.29  (*List of previous goal stacks, for the undo operation.  Set by setstate. 
    1.30 @@ -124,13 +124,13 @@
    1.31  (*Common treatment of "goal" and "prove_goal":
    1.32    Return assumptions, initial proof state, and function to make result. *)
    1.33  fun prepare_proof rths chorn =
    1.34 -  let val {sign, t=horn,...} = Sign.rep_cterm chorn;
    1.35 +  let val {sign, t=horn,...} = rep_cterm chorn;
    1.36        val (_,As,B) = Logic.strip_horn(horn);
    1.37 -      val cAs = map (Sign.cterm_of sign) As;
    1.38 +      val cAs = map (cterm_of sign) As;
    1.39        val p_rew = if null rths then I else rewrite_rule rths;
    1.40        val c_rew = if null rths then I else rewrite_goals_rule rths;
    1.41        val prems = map (p_rew o forall_elim_vars(0) o assume) cAs
    1.42 -      and st0 = c_rew (trivial (Sign.cterm_of sign B))
    1.43 +      and st0 = c_rew (trivial (cterm_of sign B))
    1.44        fun result_error state msg = 
    1.45          (writeln ("Bad final proof state:");
    1.46   	 !print_goals_ref (!goals_limit) state;
    1.47 @@ -151,7 +151,7 @@
    1.48                  ("Additional hypotheses:\n" ^ 
    1.49                   cat_lines (map (Sign.string_of_term sign) hyps))
    1.50  	    else if Pattern.eta_matches (#tsig(Sign.rep_sg sign)) 
    1.51 -			                (Sign.term_of chorn, prop)
    1.52 +			                (term_of chorn, prop)
    1.53  		 then  standard th 
    1.54  	    else  result_error state "proved a different theorem"
    1.55          end
    1.56 @@ -199,7 +199,7 @@
    1.57  (*Version taking the goal as a string*)
    1.58  fun prove_goalw thy rths agoal tacsf =
    1.59    let val sign = sign_of thy
    1.60 -      val chorn = Sign.read_cterm sign (agoal,propT)
    1.61 +      val chorn = read_cterm sign (agoal,propT)
    1.62    in  prove_goalw_cterm rths chorn tacsf  
    1.63        handle ERROR => error (*from type_assign, etc via prepare_proof*)
    1.64  		("The error above occurred for " ^ quote agoal)
    1.65 @@ -286,7 +286,7 @@
    1.66      Initial subgoal and premises are rewritten using rths. **)
    1.67  
    1.68  (*Version taking the goal as a cterm; if you have a term t and theory thy, use
    1.69 -    goalw_cterm rths (Sign.cterm_of (sign_of thy) t);      *)
    1.70 +    goalw_cterm rths (cterm_of (sign_of thy) t);      *)
    1.71  fun goalw_cterm rths chorn = 
    1.72    let val (prems, st0, mkresult) = prepare_proof rths chorn
    1.73    in  undo_list := [];
    1.74 @@ -298,7 +298,7 @@
    1.75  
    1.76  (*Version taking the goal as a string*)
    1.77  fun goalw thy rths agoal = 
    1.78 -  goalw_cterm rths (Sign.read_cterm(sign_of thy)(agoal,propT))
    1.79 +  goalw_cterm rths (read_cterm(sign_of thy)(agoal,propT))
    1.80    handle ERROR => error (*from type_assign, etc via prepare_proof*)
    1.81  	    ("The error above occurred for " ^ quote agoal);
    1.82  
    1.83 @@ -418,7 +418,7 @@
    1.84  
    1.85  fun top_sg() = #sign(rep_thm(topthm()));
    1.86  
    1.87 -fun read s = Sign.term_of (Sign.read_cterm (top_sg())
    1.88 +fun read s = term_of (read_cterm (top_sg())
    1.89  			                   (s, (TVar(("DUMMY",0),[]))));
    1.90  
    1.91  (*Print a term under the current signature of the proof state*)
     2.1 --- a/src/Pure/install_pp.ML	Tue Jan 18 13:46:08 1994 +0100
     2.2 +++ b/src/Pure/install_pp.ML	Tue Jan 18 15:57:40 1994 +0100
     2.3 @@ -4,12 +4,12 @@
     2.4  Set up automatic toplevel printing
     2.5  *)
     2.6  
     2.7 -install_pp (make_pp ["Thm", "thm"] pprint_thm);
     2.8 -install_pp (make_pp ["Thm", "theory"] pprint_theory);
     2.9 -install_pp (make_pp ["Sign", "sg"] pprint_sg);
    2.10 -install_pp (make_pp ["Sign", "cterm"] Sign.pprint_cterm);
    2.11 -install_pp (make_pp ["Sign", "ctyp"] Sign.pprint_ctyp);
    2.12 -install_pp (make_pp ["Syntax", "ast"] Syntax.pprint_ast);
    2.13 +install_pp (make_pp ["Thm", "thm"] 	pprint_thm);
    2.14 +install_pp (make_pp ["Thm", "theory"] 	pprint_theory);
    2.15 +install_pp (make_pp ["Thm", "cterm"] 	pprint_cterm);
    2.16 +install_pp (make_pp ["Thm", "ctyp"] 	pprint_ctyp);
    2.17 +install_pp (make_pp ["Sign", "sg"] 	pprint_sg);
    2.18 +install_pp (make_pp ["Syntax", "ast"] 	Syntax.pprint_ast);
    2.19  
    2.20  (*
    2.21  install_pp (make_pp ["term"] pprint_term);
     3.1 --- a/src/Pure/tactic.ML	Tue Jan 18 13:46:08 1994 +0100
     3.2 +++ b/src/Pure/tactic.ML	Tue Jan 18 15:57:40 1994 +0100
     3.3 @@ -99,8 +99,8 @@
     3.4    let val fth = freezeT th
     3.5        val {prop,sign,...} = rep_thm fth
     3.6        fun mk_inst (Var(v,T)) = 
     3.7 -	  (Sign.cterm_of sign (Var(v,T)),
     3.8 -	   Sign.cterm_of sign (Free(string_of v, T)))
     3.9 +	  (cterm_of sign (Var(v,T)),
    3.10 +	   cterm_of sign (Free(string_of v, T)))
    3.11        val insts = map mk_inst (term_vars prop)
    3.12    in  instantiate ([],insts) fth  end;
    3.13  
    3.14 @@ -184,14 +184,14 @@
    3.15      fun liftterm t = list_abs_free (params, 
    3.16  				    Logic.incr_indexes(paramTs,inc) t)
    3.17      (*Lifts instantiation pair over params*)
    3.18 -    fun liftpair (cv,ct) = (Sign.cfun liftvar cv, Sign.cfun liftterm ct)
    3.19 +    fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct)
    3.20      fun lifttvar((a,i),ctyp) =
    3.21 -	let val {T,sign} = Sign.rep_ctyp ctyp
    3.22 -	in  ((a,i+inc), Sign.ctyp_of sign (incr_tvar inc T)) end
    3.23 +	let val {T,sign} = rep_ctyp ctyp
    3.24 +	in  ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end
    3.25      val rts = types_sorts rule and (types,sorts) = types_sorts state
    3.26      fun types'(a,~1) = (case assoc(params,a) of None => types(a,~1) | sm => sm)
    3.27        | types'(ixn) = types ixn;
    3.28 -    val (Tinsts,insts) = Sign.read_insts sign rts (types',sorts) sinsts
    3.29 +    val (Tinsts,insts) = read_insts sign rts (types',sorts) sinsts
    3.30  in instantiate (map lifttvar Tinsts, map liftpair insts)
    3.31  		(lift_rule (state,i) rule)
    3.32  end;
     4.1 --- a/src/Pure/tctical.ML	Tue Jan 18 13:46:08 1994 +0100
     4.2 +++ b/src/Pure/tctical.ML	Tue Jan 18 15:57:40 1994 +0100
     4.3 @@ -399,7 +399,7 @@
     4.4  (* (!!x. PROP ?V) ==> PROP ?V ;  contains NO TYPE VARIABLES.*)
     4.5  val dummy_quant_rl = 
     4.6    standard (forall_elim_var 0 (assume 
     4.7 -                  (Sign.read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
     4.8 +                  (read_cterm Sign.pure ("!!x::prop. PROP V",propT))));
     4.9  
    4.10  (* Prevent the subgoal's assumptions from becoming additional subgoals in the
    4.11     new proof state by enclosing them by a universal quantification *)
    4.12 @@ -411,7 +411,7 @@
    4.13  (*Does the work of SELECT_GOAL. *)
    4.14  fun select (Tactic tf) state i =
    4.15    let val prem::_ = drop(i-1, prems_of state)
    4.16 -      val st0 = trivial (Sign.cterm_of (#sign(rep_thm state)) prem);
    4.17 +      val st0 = trivial (cterm_of (#sign(rep_thm state)) prem);
    4.18        fun next st = bicompose false (false, st, nprems_of st) i state
    4.19    in  Sequence.flats (Sequence.maps next (tf st0))
    4.20    end;
    4.21 @@ -469,7 +469,7 @@
    4.22  
    4.23  fun metahyps_aux_tac tacf (prem,i) = Tactic (fn state =>
    4.24    let val {sign,maxidx,...} = rep_thm state
    4.25 -      val cterm = Sign.cterm_of sign
    4.26 +      val cterm = cterm_of sign
    4.27        (*find all vars in the hyps -- should find tvars also!*)
    4.28        val hyps_vars = foldr add_term_vars (strip_assums_hyp prem, [])
    4.29        val insts = map mk_inst hyps_vars