renamed Term.variant_abs to Syntax.variant_abs;
authorwenzelm
Tue Jul 25 21:18:00 2006 +0200 (2006-07-25)
changeset 20194c9dbce9a23a1
parent 20193 46f5ef758422
child 20195 ae79b9ad7224
renamed Term.variant_abs to Syntax.variant_abs;
src/FOLP/simp.ML
src/HOL/Integ/cooper_dec.ML
src/HOL/Integ/presburger.ML
src/HOL/Integ/qelim.ML
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Real/ferrante_rackoff_proof.ML
src/HOL/Tools/Presburger/cooper_dec.ML
src/HOL/Tools/Presburger/presburger.ML
src/HOL/Tools/Presburger/qelim.ML
src/HOLCF/IOA/meta_theory/ioa_package.ML
src/Pure/Tools/codegen_package.ML
src/Pure/tctical.ML
     1.1 --- a/src/FOLP/simp.ML	Tue Jul 25 21:17:58 2006 +0200
     1.2 +++ b/src/FOLP/simp.ML	Tue Jul 25 21:18:00 2006 +0200
     1.3 @@ -377,7 +377,7 @@
     1.4  (*Replace parameters by Free variables in P*)
     1.5  fun variants_abs ([],P) = P
     1.6    | variants_abs ((a,T)::aTs, P) =
     1.7 -      variants_abs (aTs, #2 (variant_abs(a,T,P)));
     1.8 +      variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
     1.9  
    1.10  (*Select subgoal i from proof state; substitute parameters, for printing*)
    1.11  fun prepare_goal i st =
     2.1 --- a/src/HOL/Integ/cooper_dec.ML	Tue Jul 25 21:17:58 2006 +0200
     2.2 +++ b/src/HOL/Integ/cooper_dec.ML	Tue Jul 25 21:18:00 2006 +0200
     2.3 @@ -675,7 +675,7 @@
     2.4    case fm of 
     2.5     Const ("Ex",_) $ Abs(x0,T,p0) => 
     2.6     let 
     2.7 -    val (xn,p1) = variant_abs (x0,T,p0) 
     2.8 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0) 
     2.9      val x = Free (xn,T)  
    2.10      val vars = (xn::vars1) 
    2.11      val p = unitycoeff x  (posineq (simpl p1))
    2.12 @@ -694,7 +694,7 @@
    2.13  fun cooperpi vars1 fm =
    2.14    case fm of
    2.15     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    2.16 -    val (xn,p1) = variant_abs (x0,T,p0)
    2.17 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    2.18      val x = Free (xn,T)
    2.19      val vars = (xn::vars1)
    2.20      val p = unitycoeff x  (posineq (simpl p1))
    2.21 @@ -759,7 +759,7 @@
    2.22  fun cooper vars1 fm =
    2.23    case fm of
    2.24     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    2.25 -    val (xn,p1) = variant_abs (x0,T,p0)
    2.26 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    2.27      val x = Free (xn,T)
    2.28      val vars = (xn::vars1)
    2.29  (*     val p = unitycoeff x  (posineq (simpl p1)) *)
    2.30 @@ -794,7 +794,7 @@
    2.31  fun cooper_w vars1 fm =
    2.32    case fm of
    2.33     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    2.34 -    val (xn,p1) = variant_abs (x0,T,p0)
    2.35 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    2.36      val x = Free (xn,T)
    2.37      val vars = (xn::vars1)
    2.38  (*     val p = unitycoeff x  (posineq (simpl p1)) *)
     3.1 --- a/src/HOL/Integ/presburger.ML	Tue Jul 25 21:17:58 2006 +0200
     3.2 +++ b/src/HOL/Integ/presburger.ML	Tue Jul 25 21:18:00 2006 +0200
     3.3 @@ -65,7 +65,7 @@
     3.4  	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
     3.5  
     3.6  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
     3.7 -  let val (xn1,p1) = variant_abs (xn,xT,p)
     3.8 +  let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
     3.9    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    3.10  
    3.11  fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
     4.1 --- a/src/HOL/Integ/qelim.ML	Tue Jul 25 21:17:58 2006 +0200
     4.2 +++ b/src/HOL/Integ/qelim.ML	Tue Jul 25 21:18:00 2006 +0200
     4.3 @@ -40,7 +40,7 @@
     4.4     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
     4.5     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
     4.6     |(Const("Ex",_)$Abs(xn,xT,p)) => 
     4.7 -      let val (xn1,p1) = variant_abs(xn,xT,p) 
     4.8 +      let val (xn1,p1) = Syntax.variant_abs(xn,xT,p) 
     4.9        in ([p1],
    4.10          fn [th1_1] => 
    4.11            let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
     5.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 25 21:17:58 2006 +0200
     5.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Tue Jul 25 21:18:00 2006 +0200
     5.3 @@ -51,7 +51,7 @@
     5.4  		        else (contains_if b) |
     5.5    contains_if _ = [];
     5.6  
     5.7 -  fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(variant_abs(a,T,t))) |
     5.8 +  fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(Syntax.variant_abs(a,T,t))) |
     5.9    find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then
    5.10    (if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b))
    5.11    else (a $ b,contains_if(a $ b))|
    5.12 @@ -167,7 +167,7 @@
    5.13  fun type_of_term (Const(_,t)) = t |
    5.14  type_of_term (Free(_,t)) = t |
    5.15  type_of_term (Var(_,t)) = t |
    5.16 -type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(variant_abs(x,t,trm)))]) |
    5.17 +type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(Syntax.variant_abs(x,t,trm)))]) |
    5.18  type_of_term (a $ b) =
    5.19  let
    5.20   fun accept_fun_type (Type("fun",[x,y])) = (x,y) |
    5.21 @@ -322,7 +322,7 @@
    5.22    | dest_atom (Free t)  = dest_Free (Free t);
    5.23  
    5.24  fun get_decls sign Clist (Abs(s,tp,trm)) = 
    5.25 -    let val VarAbs = variant_abs(s,tp,trm);
    5.26 +    let val VarAbs = Syntax.variant_abs(s,tp,trm);
    5.27      in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
    5.28      end
    5.29    | get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
    5.30 @@ -429,7 +429,7 @@
    5.31  fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) =
    5.32      (let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]);
    5.33       	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
    5.34 -	 val VarAbs = variant_abs(str,tp,t);
    5.35 +	 val VarAbs = Syntax.variant_abs(str,tp,t);
    5.36  	 val BoundConst = Const(fst VarAbs,tp);
    5.37  	 val t1 = ExConst $ TypeConst;
    5.38  	 val t2 = t1 $ BoundConst;
    5.39 @@ -438,7 +438,7 @@
    5.40    |  elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) =
    5.41      (let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]);
    5.42      	 val TypeConst = Const (type_to_string_OUTPUT tp,tp);
    5.43 -	 val VarAbs = variant_abs(str,tp,t);
    5.44 +	 val VarAbs = Syntax.variant_abs(str,tp,t);
    5.45  	 val BoundConst = Const(fst VarAbs,tp);
    5.46  	 val t1 = AllConst $ TypeConst;
    5.47  	 val t2 = t1 $ BoundConst;
    5.48 @@ -606,7 +606,7 @@
    5.49  fun enrich_case_with_terms sg [] t = t |
    5.50  enrich_case_with_terms sg [trm] (Abs(x,T,t)) =
    5.51  let
    5.52 - val v = variant_abs(x,T,t);
    5.53 + val v = Syntax.variant_abs(x,T,t);
    5.54   val f = fst v;
    5.55   val s = snd v
    5.56  in
    5.57 @@ -634,7 +634,7 @@
    5.58  
    5.59  fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t = 
    5.60  let
    5.61 - fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(variant_abs(x,T,t))) |
    5.62 + fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(Syntax.variant_abs(x,T,t))) |
    5.63   heart_of_trm t = t;
    5.64   fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) |
    5.65   replace_termlist_with_args sg _ trm _ [a] _ ([],[]) =
    5.66 @@ -704,7 +704,7 @@
    5.67  replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) |
    5.68  replace_case sg tl (Abs(x,T,t)) _ = 
    5.69  let 
    5.70 - val v = variant_abs(x,T,t);
    5.71 + val v = Syntax.variant_abs(x,T,t);
    5.72   val f = fst v;
    5.73   val s = snd v
    5.74  in
    5.75 @@ -779,9 +779,9 @@
    5.76    else (constr_term_contains_var sg tl b x))
    5.77  end |
    5.78  constr_term_contains_var sg tl (Abs(y,ty,trm)) x =
    5.79 -         constr_term_contains_var sg tl (snd(variant_abs(y,ty,trm))) x |
    5.80 +         constr_term_contains_var sg tl (snd(Syntax.variant_abs(y,ty,trm))) x |
    5.81  constr_term_contains_var _ _ _ _ = false;
    5.82 -val vt = variant_abs(x,ty,trm);
    5.83 +val vt = Syntax.variant_abs(x,ty,trm);
    5.84  val tt = remove_vars sg tl (snd(vt))
    5.85  in
    5.86  if (constr_term_contains_var sg tl tt (fst vt))
     6.1 --- a/src/HOL/Real/ferrante_rackoff_proof.ML	Tue Jul 25 21:17:58 2006 +0200
     6.2 +++ b/src/HOL/Real/ferrante_rackoff_proof.ML	Tue Jul 25 21:18:00 2006 +0200
     6.3 @@ -212,7 +212,7 @@
     6.4  fun ferrack_eq thy p = 
     6.5      case p of
     6.6          Const("Ex",_)$Abs(x1,T,p1) => 
     6.7 -        let val (xn,fm) = variant_abs(x1,T,p1)
     6.8 +        let val (xn,fm) = Syntax.variant_abs(x1,T,p1)
     6.9              val x = Free(xn,T)
    6.10              val (u,cu,uths,uf) = inusetthms thy x fm
    6.11              val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
    6.12 @@ -625,7 +625,7 @@
    6.13          ([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
    6.14        | (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
    6.15        | (Const("Ex",_)$Abs(xn,xT,p)) => 
    6.16 -        let val (xn1,p1) = variant_abs(xn,xT,p)
    6.17 +        let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
    6.18              val x= Free(xn1,xT)
    6.19          in ([(p1,x::vs)],
    6.20              fn [th1_1] => 
     7.1 --- a/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jul 25 21:17:58 2006 +0200
     7.2 +++ b/src/HOL/Tools/Presburger/cooper_dec.ML	Tue Jul 25 21:18:00 2006 +0200
     7.3 @@ -675,7 +675,7 @@
     7.4    case fm of 
     7.5     Const ("Ex",_) $ Abs(x0,T,p0) => 
     7.6     let 
     7.7 -    val (xn,p1) = variant_abs (x0,T,p0) 
     7.8 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0) 
     7.9      val x = Free (xn,T)  
    7.10      val vars = (xn::vars1) 
    7.11      val p = unitycoeff x  (posineq (simpl p1))
    7.12 @@ -694,7 +694,7 @@
    7.13  fun cooperpi vars1 fm =
    7.14    case fm of
    7.15     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    7.16 -    val (xn,p1) = variant_abs (x0,T,p0)
    7.17 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    7.18      val x = Free (xn,T)
    7.19      val vars = (xn::vars1)
    7.20      val p = unitycoeff x  (posineq (simpl p1))
    7.21 @@ -759,7 +759,7 @@
    7.22  fun cooper vars1 fm =
    7.23    case fm of
    7.24     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    7.25 -    val (xn,p1) = variant_abs (x0,T,p0)
    7.26 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    7.27      val x = Free (xn,T)
    7.28      val vars = (xn::vars1)
    7.29  (*     val p = unitycoeff x  (posineq (simpl p1)) *)
    7.30 @@ -794,7 +794,7 @@
    7.31  fun cooper_w vars1 fm =
    7.32    case fm of
    7.33     Const ("Ex",_) $ Abs(x0,T,p0) => let 
    7.34 -    val (xn,p1) = variant_abs (x0,T,p0)
    7.35 +    val (xn,p1) = Syntax.variant_abs (x0,T,p0)
    7.36      val x = Free (xn,T)
    7.37      val vars = (xn::vars1)
    7.38  (*     val p = unitycoeff x  (posineq (simpl p1)) *)
     8.1 --- a/src/HOL/Tools/Presburger/presburger.ML	Tue Jul 25 21:17:58 2006 +0200
     8.2 +++ b/src/HOL/Tools/Presburger/presburger.ML	Tue Jul 25 21:18:00 2006 +0200
     8.3 @@ -65,7 +65,7 @@
     8.4  	    @ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
     8.5  
     8.6  fun cooper_pp sg (fm as e$Abs(xn,xT,p)) = 
     8.7 -  let val (xn1,p1) = variant_abs (xn,xT,p)
     8.8 +  let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
     8.9    in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
    8.10  
    8.11  fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
     9.1 --- a/src/HOL/Tools/Presburger/qelim.ML	Tue Jul 25 21:17:58 2006 +0200
     9.2 +++ b/src/HOL/Tools/Presburger/qelim.ML	Tue Jul 25 21:18:00 2006 +0200
     9.3 @@ -40,7 +40,7 @@
     9.4     |(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
     9.5     |(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
     9.6     |(Const("Ex",_)$Abs(xn,xT,p)) => 
     9.7 -      let val (xn1,p1) = variant_abs(xn,xT,p) 
     9.8 +      let val (xn1,p1) = Syntax.variant_abs(xn,xT,p) 
     9.9        in ([p1],
    9.10          fn [th1_1] => 
    9.11            let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
    10.1 --- a/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 25 21:17:58 2006 +0200
    10.2 +++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML	Tue Jul 25 21:18:00 2006 +0200
    10.3 @@ -78,7 +78,7 @@
    10.4  extract_hd (Const(s,_)) = s |
    10.5  extract_hd _ = raise malformed;
    10.6  (* delivers constructor term string from a prem of *.induct *)
    10.7 -fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))|
    10.8 +fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
    10.9  extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
   10.10  extract_constr thy (Var(_,_) $ r) =  delete_bold_string(string_of_term (sign_of thy) r) |
   10.11  extract_constr _ _ = raise malformed;
    11.1 --- a/src/Pure/Tools/codegen_package.ML	Tue Jul 25 21:17:58 2006 +0200
    11.2 +++ b/src/Pure/Tools/codegen_package.ML	Tue Jul 25 21:18:00 2006 +0200
    11.3 @@ -756,7 +756,7 @@
    11.4        |-> (fn ty => pair (IVar v))
    11.5    | exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
    11.6        let
    11.7 -        val (v, t) = Term.variant_abs (Symbol.alphanum raw_v, ty, raw_t);
    11.8 +        val (v, t) = Syntax.variant_abs (Symbol.alphanum raw_v, ty, raw_t);
    11.9        in
   11.10          trns
   11.11          |> exprgen_type thy tabs ty
    12.1 --- a/src/Pure/tctical.ML	Tue Jul 25 21:17:58 2006 +0200
    12.2 +++ b/src/Pure/tctical.ML	Tue Jul 25 21:18:00 2006 +0200
    12.3 @@ -375,7 +375,7 @@
    12.4  fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
    12.5          strip_context_aux (params, H::Hs, B)
    12.6    | strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
    12.7 -        let val (b,u) = variant_abs(a,T,t)
    12.8 +        let val (b,u) = Syntax.variant_abs(a,T,t)
    12.9          in  strip_context_aux ((b,T)::params, Hs, u)  end
   12.10    | strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);
   12.11