--- a/src/FOLP/simp.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/FOLP/simp.ML Tue Jul 25 21:18:00 2006 +0200
@@ -377,7 +377,7 @@
(*Replace parameters by Free variables in P*)
fun variants_abs ([],P) = P
| variants_abs ((a,T)::aTs, P) =
- variants_abs (aTs, #2 (variant_abs(a,T,P)));
+ variants_abs (aTs, #2 (Syntax.variant_abs(a,T,P)));
(*Select subgoal i from proof state; substitute parameters, for printing*)
fun prepare_goal i st =
--- a/src/HOL/Integ/cooper_dec.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Integ/cooper_dec.ML Tue Jul 25 21:18:00 2006 +0200
@@ -675,7 +675,7 @@
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) =>
let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
val p = unitycoeff x (posineq (simpl p1))
@@ -694,7 +694,7 @@
fun cooperpi vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
val p = unitycoeff x (posineq (simpl p1))
@@ -759,7 +759,7 @@
fun cooper vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
(* val p = unitycoeff x (posineq (simpl p1)) *)
@@ -794,7 +794,7 @@
fun cooper_w vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
(* val p = unitycoeff x (posineq (simpl p1)) *)
--- a/src/HOL/Integ/presburger.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Integ/presburger.ML Tue Jul 25 21:18:00 2006 +0200
@@ -65,7 +65,7 @@
@ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
- let val (xn1,p1) = variant_abs (xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
--- a/src/HOL/Integ/qelim.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Integ/qelim.ML Tue Jul 25 21:18:00 2006 +0200
@@ -40,7 +40,7 @@
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
|(Const("Ex",_)$Abs(xn,xT,p)) =>
- let val (xn1,p1) = variant_abs(xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
in ([p1],
fn [th1_1] =>
let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
--- a/src/HOL/Modelcheck/mucke_oracle.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Tue Jul 25 21:18:00 2006 +0200
@@ -51,7 +51,7 @@
else (contains_if b) |
contains_if _ = [];
- fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(variant_abs(a,T,t))) |
+ fun find_replace_term (Abs(a,T,t)) = find_replace_term (snd(Syntax.variant_abs(a,T,t))) |
find_replace_term (a $ b) = if ((contains_if (a $ b))=[]) then
(if (snd(find_replace_term b)=[]) then (find_replace_term a) else (find_replace_term b))
else (a $ b,contains_if(a $ b))|
@@ -167,7 +167,7 @@
fun type_of_term (Const(_,t)) = t |
type_of_term (Free(_,t)) = t |
type_of_term (Var(_,t)) = t |
-type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(variant_abs(x,t,trm)))]) |
+type_of_term (Abs(x,t,trm)) = Type("fun",[t,type_of_term(snd(Syntax.variant_abs(x,t,trm)))]) |
type_of_term (a $ b) =
let
fun accept_fun_type (Type("fun",[x,y])) = (x,y) |
@@ -322,7 +322,7 @@
| dest_atom (Free t) = dest_Free (Free t);
fun get_decls sign Clist (Abs(s,tp,trm)) =
- let val VarAbs = variant_abs(s,tp,trm);
+ let val VarAbs = Syntax.variant_abs(s,tp,trm);
in get_decls sign (Const(fst VarAbs,tp)::Clist) (snd VarAbs)
end
| get_decls sign Clist ((Const("split",_)) $ trm) = get_decls sign Clist trm
@@ -429,7 +429,7 @@
fun elim_quantifications sign ((Const("Ex",_)) $ Abs (str,tp,t)) =
(let val ExConst = Const("_Ex",make_fun_type [tp,tp,tp,tp]);
val TypeConst = Const (type_to_string_OUTPUT tp,tp);
- val VarAbs = variant_abs(str,tp,t);
+ val VarAbs = Syntax.variant_abs(str,tp,t);
val BoundConst = Const(fst VarAbs,tp);
val t1 = ExConst $ TypeConst;
val t2 = t1 $ BoundConst;
@@ -438,7 +438,7 @@
| elim_quantifications sign ((Const("All",_)) $ Abs (str,tp,t)) =
(let val AllConst = Const("_All",make_fun_type [tp,tp,tp,tp]);
val TypeConst = Const (type_to_string_OUTPUT tp,tp);
- val VarAbs = variant_abs(str,tp,t);
+ val VarAbs = Syntax.variant_abs(str,tp,t);
val BoundConst = Const(fst VarAbs,tp);
val t1 = AllConst $ TypeConst;
val t2 = t1 $ BoundConst;
@@ -606,7 +606,7 @@
fun enrich_case_with_terms sg [] t = t |
enrich_case_with_terms sg [trm] (Abs(x,T,t)) =
let
- val v = variant_abs(x,T,t);
+ val v = Syntax.variant_abs(x,T,t);
val f = fst v;
val s = snd v
in
@@ -634,7 +634,7 @@
fun replace_termlist_with_constrs sg tl (a::l1) (c::l2) t =
let
- fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(variant_abs(x,T,t))) |
+ fun heart_of_trm (Abs(x,T,t)) = heart_of_trm(snd(Syntax.variant_abs(x,T,t))) |
heart_of_trm t = t;
fun replace_termlist_with_args _ _ trm _ [] _ ([],[]) = trm (* should never occur *) |
replace_termlist_with_args sg _ trm _ [a] _ ([],[]) =
@@ -704,7 +704,7 @@
replace_case sg tl (a $ b) n = (replace_case sg tl a (n-1)) $ (replace_case sg tl b 0) |
replace_case sg tl (Abs(x,T,t)) _ =
let
- val v = variant_abs(x,T,t);
+ val v = Syntax.variant_abs(x,T,t);
val f = fst v;
val s = snd v
in
@@ -779,9 +779,9 @@
else (constr_term_contains_var sg tl b x))
end |
constr_term_contains_var sg tl (Abs(y,ty,trm)) x =
- constr_term_contains_var sg tl (snd(variant_abs(y,ty,trm))) x |
+ constr_term_contains_var sg tl (snd(Syntax.variant_abs(y,ty,trm))) x |
constr_term_contains_var _ _ _ _ = false;
-val vt = variant_abs(x,ty,trm);
+val vt = Syntax.variant_abs(x,ty,trm);
val tt = remove_vars sg tl (snd(vt))
in
if (constr_term_contains_var sg tl tt (fst vt))
--- a/src/HOL/Real/ferrante_rackoff_proof.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Real/ferrante_rackoff_proof.ML Tue Jul 25 21:18:00 2006 +0200
@@ -212,7 +212,7 @@
fun ferrack_eq thy p =
case p of
Const("Ex",_)$Abs(x1,T,p1) =>
- let val (xn,fm) = variant_abs(x1,T,p1)
+ let val (xn,fm) = Syntax.variant_abs(x1,T,p1)
val x = Free(xn,T)
val (u,cu,uths,uf) = inusetthms thy x fm
val (mi,pi,nmi,npi,lind) = divide_and_conquer (decomp_mpinf thy x (u,cu,uths)) fm
@@ -625,7 +625,7 @@
([(A,vs),(B,vs)], fn [th1,th2] => [th1,th2] MRS qe_eqI)
| (Const("Not",_)$p) => ([(p,vs)],fn [th] => th RS qe_Not)
| (Const("Ex",_)$Abs(xn,xT,p)) =>
- let val (xn1,p1) = variant_abs(xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
val x= Free(xn1,xT)
in ([(p1,x::vs)],
fn [th1_1] =>
--- a/src/HOL/Tools/Presburger/cooper_dec.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Tools/Presburger/cooper_dec.ML Tue Jul 25 21:18:00 2006 +0200
@@ -675,7 +675,7 @@
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) =>
let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
val p = unitycoeff x (posineq (simpl p1))
@@ -694,7 +694,7 @@
fun cooperpi vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
val p = unitycoeff x (posineq (simpl p1))
@@ -759,7 +759,7 @@
fun cooper vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
(* val p = unitycoeff x (posineq (simpl p1)) *)
@@ -794,7 +794,7 @@
fun cooper_w vars1 fm =
case fm of
Const ("Ex",_) $ Abs(x0,T,p0) => let
- val (xn,p1) = variant_abs (x0,T,p0)
+ val (xn,p1) = Syntax.variant_abs (x0,T,p0)
val x = Free (xn,T)
val vars = (xn::vars1)
(* val p = unitycoeff x (posineq (simpl p1)) *)
--- a/src/HOL/Tools/Presburger/presburger.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Tools/Presburger/presburger.ML Tue Jul 25 21:18:00 2006 +0200
@@ -65,7 +65,7 @@
@ powerarith @[thm"not_false_eq_true", thm "not_true_eq_false"];
fun cooper_pp sg (fm as e$Abs(xn,xT,p)) =
- let val (xn1,p1) = variant_abs (xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs (xn,xT,p)
in (CooperProof.cooper_prv sg (Free (xn1, xT)) p1) end;
fun mnnf_pp sg fm = CooperProof.proof_of_cnnf sg fm
--- a/src/HOL/Tools/Presburger/qelim.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOL/Tools/Presburger/qelim.ML Tue Jul 25 21:18:00 2006 +0200
@@ -40,7 +40,7 @@
|(Const("op =", Type ("fun",[Type ("bool", []),_]))$A$B) => ([A,B], fn [th1,th2] => [th1,th2] MRS qe_eqI)
|(Const("Not",_)$p) => ([p],fn [th] => th RS qe_Not)
|(Const("Ex",_)$Abs(xn,xT,p)) =>
- let val (xn1,p1) = variant_abs(xn,xT,p)
+ let val (xn1,p1) = Syntax.variant_abs(xn,xT,p)
in ([p1],
fn [th1_1] =>
let val th2 = [th1_1,nfnp (snd (qe_get_terms th1_1))] MRS trans
--- a/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/HOLCF/IOA/meta_theory/ioa_package.ML Tue Jul 25 21:18:00 2006 +0200
@@ -78,7 +78,7 @@
extract_hd (Const(s,_)) = s |
extract_hd _ = raise malformed;
(* delivers constructor term string from a prem of *.induct *)
-fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(variant_abs(a,T,r)))|
+fun extract_constr thy (_ $ Abs(a,T,r)) = extract_constr thy (snd(Syntax.variant_abs(a,T,r)))|
extract_constr thy (Const("Trueprop",_) $ r) = extract_constr thy r |
extract_constr thy (Var(_,_) $ r) = delete_bold_string(string_of_term (sign_of thy) r) |
extract_constr _ _ = raise malformed;
--- a/src/Pure/Tools/codegen_package.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/Pure/Tools/codegen_package.ML Tue Jul 25 21:18:00 2006 +0200
@@ -756,7 +756,7 @@
|-> (fn ty => pair (IVar v))
| exprgen_term thy tabs (Abs (raw_v, ty, raw_t)) trns =
let
- val (v, t) = Term.variant_abs (Symbol.alphanum raw_v, ty, raw_t);
+ val (v, t) = Syntax.variant_abs (Symbol.alphanum raw_v, ty, raw_t);
in
trns
|> exprgen_type thy tabs ty
--- a/src/Pure/tctical.ML Tue Jul 25 21:17:58 2006 +0200
+++ b/src/Pure/tctical.ML Tue Jul 25 21:18:00 2006 +0200
@@ -375,7 +375,7 @@
fun strip_context_aux (params, Hs, Const("==>", _) $ H $ B) =
strip_context_aux (params, H::Hs, B)
| strip_context_aux (params, Hs, Const("all",_)$Abs(a,T,t)) =
- let val (b,u) = variant_abs(a,T,t)
+ let val (b,u) = Syntax.variant_abs(a,T,t)
in strip_context_aux ((b,T)::params, Hs, u) end
| strip_context_aux (params, Hs, B) = (rev params, rev Hs, B);