--- a/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Decision_Procs/Approximation.thy Thu Jun 10 12:24:03 2010 +0200
@@ -3440,7 +3440,7 @@
fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
fun dest_ivl (Const (@{const_name "Some"}, _) $
- (Const (@{const_name "Pair"}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
+ (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
| dest_ivl (Const (@{const_name "None"}, _)) = NONE
| dest_ivl t = raise TERM ("dest_result", [t])
--- a/src/HOL/Hoare/hoare_tac.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Hoare/hoare_tac.ML Thu Jun 10 12:24:03 2010 +0200
@@ -41,9 +41,9 @@
else let val (n, T) = dest_Free x ;
val z = mk_bodyC xs;
val T2 = case z of Free(_, T) => T
- | Const ("Pair", Type ("fun", [_, Type
+ | Const (@{const_name Pair}, Type ("fun", [_, Type
("fun", [_, T])])) $ _ $ _ => T;
- in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
+ in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
(** maps a subgoal of the form:
VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy Thu Jun 10 12:24:03 2010 +0200
@@ -123,7 +123,7 @@
import_theory pair;
type_maps
- prod > "*";
+ prod > "Product_Type.*";
const_maps
"," > Pair
--- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy Thu Jun 10 12:24:03 2010 +0200
@@ -38,9 +38,9 @@
bool > bool
fun > fun
N_1 > Product_Type.unit
- prod > "*"
- num > nat
- sum > "+"
+ prod > "Product_Type.*"
+ num > Nat.nat
+ sum > "Sum_Type.+"
(* option > Datatype.option*);
const_renames
--- a/src/HOL/Import/HOL/pair.imp Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Import/HOL/pair.imp Thu Jun 10 12:24:03 2010 +0200
@@ -7,17 +7,17 @@
"LEX" > "LEX_def"
type_maps
- "prod" > "*"
+ "prod" > "Product_Type.*"
const_maps
- "pair_case" > "split"
- "UNCURRY" > "split"
- "SND" > "snd"
+ "pair_case" > "Product_Type.split"
+ "UNCURRY" > "Product_Type.split"
+ "FST" > "Product_Type.fst"
+ "SND" > "Product_Type.snd"
"RPROD" > "HOL4Base.pair.RPROD"
"LEX" > "HOL4Base.pair.LEX"
- "FST" > "fst"
"CURRY" > "Product_Type.curry"
- "," > "Pair"
+ "," > "Product_Type.Pair"
"##" > "prod_fun"
thm_maps
--- a/src/HOL/Import/HOLLight/hollight.imp Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Import/HOLLight/hollight.imp Thu Jun 10 12:24:03 2010 +0200
@@ -6,7 +6,7 @@
"sum" > "+"
"recspace" > "HOLLight.hollight.recspace"
"real" > "HOLLight.hollight.real"
- "prod" > "*"
+ "prod" > "Product_Type.*"
"option" > "HOLLight.hollight.option"
"num" > "Nat.nat"
"nadd" > "HOLLight.hollight.nadd"
@@ -131,7 +131,7 @@
"SUC" > "Nat.Suc"
"SUBSET" > "HOLLight.hollight.SUBSET"
"SOME" > "HOLLight.hollight.SOME"
- "SND" > "snd"
+ "SND" > "Product_Type.snd"
"SING" > "HOLLight.hollight.SING"
"SETSPEC" > "HOLLight.hollight.SETSPEC"
"REVERSE" > "HOLLight.hollight.REVERSE"
@@ -188,7 +188,7 @@
"GSPEC" > "HOLLight.hollight.GSPEC"
"GEQ" > "HOLLight.hollight.GEQ"
"GABS" > "HOLLight.hollight.GABS"
- "FST" > "fst"
+ "FST" > "Product_Type.fst"
"FNIL" > "HOLLight.hollight.FNIL"
"FINREC" > "HOLLight.hollight.FINREC"
"FINITE" > "HOLLight.hollight.FINITE"
@@ -239,7 +239,7 @@
"<" > "HOLLight.hollight.<"
"/\\" > "op &"
"-" > "Groups.minus" :: "nat => nat => nat"
- "," > "Pair"
+ "," > "Product_Type.Pair"
"+" > "Groups.plus" :: "nat => nat => nat"
"*" > "Groups.times" :: "nat => nat => nat"
"$" > "HOLLight.hollight.$"
--- a/src/HOL/Modelcheck/mucke_oracle.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Modelcheck/mucke_oracle.ML Thu Jun 10 12:24:03 2010 +0200
@@ -832,7 +832,7 @@
(* OUTPUT - relevant *)
(* transforms constructor term to a mucke-suitable output *)
-fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
+fun term_OUTPUT sg (Const(@{const_name Pair},_) $ a $ b) =
(term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
term_OUTPUT sg (Const(s,t)) = post_last_dot s |
--- a/src/HOL/Nominal/nominal_atoms.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_atoms.ML Thu Jun 10 12:24:03 2010 +0200
@@ -543,7 +543,7 @@
|> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn)
|> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(pt_proof pt_thm_nprod)
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
@@ -604,7 +604,7 @@
in
thy
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod)
|> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name])
(fs_proof fs_thm_nprod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
@@ -686,7 +686,7 @@
in
thy'
|> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
- |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
+ |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
|> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
|> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
|> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
--- a/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_datatype.ML Thu Jun 10 12:24:03 2010 +0200
@@ -121,7 +121,7 @@
val dj_cp = thm "dj_cp";
-fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
+fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
Type ("fun", [_, U])])) = (T, U);
fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
--- a/src/HOL/Nominal/nominal_permeq.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_permeq.ML Thu Jun 10 12:24:03 2010 +0200
@@ -103,7 +103,7 @@
case redex of
(* case pi o (f x) == (pi o f) (pi o x) *)
(Const("Nominal.perm",
- Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
+ Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) =>
(if (applicable_app f) then
let
val name = Long_Name.base_name n
@@ -190,8 +190,8 @@
fun perm_compose_simproc' sg ss redex =
(case redex of
(Const ("Nominal.perm", Type ("fun", [Type ("List.list",
- [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
- Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $
+ [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm",
+ Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $
pi2 $ t)) =>
let
val tname' = Long_Name.base_name tname
--- a/src/HOL/Nominal/nominal_thmdecls.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Nominal/nominal_thmdecls.ML Thu Jun 10 12:24:03 2010 +0200
@@ -103,7 +103,7 @@
let fun get_pi_aux s =
(case s of
(Const (@{const_name "perm"} ,typrm) $
- (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
+ (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
(Var (n,ty))) =>
let
(* FIXME: this should be an operation the library *)
--- a/src/HOL/Tools/Function/function_lib.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/Function/function_lib.ML Thu Jun 10 12:24:03 2010 +0200
@@ -24,7 +24,7 @@
case vars of
(Free v) => lambda (Free v) t
| (Var v) => lambda (Var v) t
- | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
+ | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
(HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
| _ => raise Match
--- a/src/HOL/Tools/Function/termination.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Jun 10 12:24:03 2010 +0200
@@ -148,7 +148,7 @@
val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
let
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
= Term.strip_qnt_body "Ex" c
in cons r o cons l end
in
@@ -185,7 +185,7 @@
val vs = Term.strip_qnt_vars "Ex" c
(* FIXME: throw error "dest_call" for malformed terms *)
- val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
+ val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
= Term.strip_qnt_body "Ex" c
val (p, l') = dest_inj sk l
val (q, r') = dest_inj sk r
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML Thu Jun 10 12:24:03 2010 +0200
@@ -265,12 +265,12 @@
fun replace_ho_args mode hoargs ts =
let
fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
- | replace (Pair (m1, m2), Const ("Pair", T) $ t1 $ t2) hoargs =
+ | replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs =
let
val (t1', hoargs') = replace (m1, t1) hoargs
val (t2', hoargs'') = replace (m2, t2) hoargs'
in
- (Const ("Pair", T) $ t1' $ t2', hoargs'')
+ (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
end
| replace (_, t) hoargs = (t, hoargs)
in
@@ -290,7 +290,7 @@
fun split_map_mode f mode ts =
let
fun split_arg_mode' (m as Fun _) t = f m t
- | split_arg_mode' (Pair (m1, m2)) (Const ("Pair", _) $ t1 $ t2) =
+ | split_arg_mode' (Pair (m1, m2)) (Const (@{const_name Pair}, _) $ t1 $ t2) =
let
val (i1, o1) = split_arg_mode' m1 t1
val (i2, o2) = split_arg_mode' m2 t2
@@ -334,7 +334,7 @@
end
| fold_map_aterms_prodT comb f T s = f T s
-fun map_filter_prod f (Const ("Pair", _) $ t1 $ t2) =
+fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
| map_filter_prod f t = f t
@@ -561,8 +561,8 @@
(* combinators to apply a function to all basic parts of nested products *)
-fun map_products f (Const ("Pair", T) $ t1 $ t2) =
- Const ("Pair", T) $ map_products f t1 $ map_products f t2
+fun map_products f (Const (@{const_name Pair}, T) $ t1 $ t2) =
+ Const (@{const_name Pair}, T) $ map_products f t1 $ map_products f t2
| map_products f t = f t
(* split theorems of case expressions *)
@@ -756,7 +756,7 @@
(case HOLogic.strip_tupleT (fastype_of arg) of
(Ts as _ :: _ :: _) =>
let
- fun rewrite_arg' (Const (@{const_name "Pair"}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
+ fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
(args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
| rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
let
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Thu Jun 10 12:24:03 2010 +0200
@@ -117,7 +117,7 @@
end;
fun dest_randomT (Type ("fun", [@{typ Random.seed},
- Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
+ Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
| dest_randomT T = raise TYPE ("dest_randomT", [T], [])
fun mk_tracing s t =
@@ -467,7 +467,7 @@
(* generation of case rules from user-given introduction rules *)
-fun mk_args2 (Type ("*", [T1, T2])) st =
+fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st =
let
val (t1, st') = mk_args2 T1 st
val (t2, st'') = mk_args2 T2 st'
@@ -1099,7 +1099,7 @@
fun all_input_of T =
let
val (Ts, U) = strip_type T
- fun input_of (Type ("*", [T1, T2])) = Pair (input_of T1, input_of T2)
+ fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2)
| input_of _ = Input
in
if U = HOLogic.boolT then
@@ -1190,7 +1190,7 @@
fun missing_vars vs t = subtract (op =) vs (term_vs t)
-fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =
+fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =
output_terms (t1, d1) @ output_terms (t2, d2)
| output_terms (t1 $ t2, Mode_App (d1, d2)) =
output_terms (t1, d1) @ output_terms (t2, d2)
@@ -1206,7 +1206,7 @@
SOME ms => SOME (map (fn m => (Context m , [])) ms)
| NONE => NONE)
-fun derivations_of (ctxt : Proof.context) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
+fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) =
map_product
(fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
(derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
@@ -1236,7 +1236,7 @@
else if eq_mode (m, Output) then
(if is_possible_output ctxt vs t then [(Term Output, [])] else [])
else []
-and all_derivations_of ctxt modes vs (Const ("Pair", _) $ t1 $ t2) =
+and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) =
let
val derivs1 = all_derivations_of ctxt modes vs t1
val derivs2 = all_derivations_of ctxt modes vs t2
@@ -1665,7 +1665,7 @@
(case (t, deriv) of
(t1 $ t2, Mode_App (deriv1, deriv2)) =>
string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
- | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
+ | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
"(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
| (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
| (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
@@ -1692,7 +1692,7 @@
val bs = map (pair "x") (binder_types (fastype_of t))
val bounds = map Bound (rev (0 upto (length bs) - 1))
in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
- | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
+ | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
(case (expr_of (t1, d1), expr_of (t2, d2)) of
(NONE, NONE) => NONE
| (NONE, SOME t) => SOME t
@@ -2010,7 +2010,7 @@
(ks @ [SOME k]))) arities));
fun split_lambda (x as Free _) t = lambda x t
- | split_lambda (Const ("Pair", _) $ t1 $ t2) t =
+ | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
| split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
| split_lambda t _ = raise (TERM ("split_lambda", [t]))
@@ -2019,7 +2019,7 @@
| strip_split_abs (Abs (_, _, t)) = strip_split_abs t
| strip_split_abs t = t
-fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names =
+fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names =
if eq_mode (m, Input) orelse eq_mode (m, Output) then
let
val x = Name.variant names "x"
@@ -3112,7 +3112,7 @@
in
if defined_functions compilation ctxt name then
let
- fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
+ fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
| extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
| extract_mode _ = Input
val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
--- a/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/TFL/dcterm.ML Thu Jun 10 12:24:03 2010 +0200
@@ -129,7 +129,7 @@
val dest_neg = dest_monop "not"
-val dest_pair = dest_binop "Pair";
+val dest_pair = dest_binop @{const_name Pair};
val dest_eq = dest_binop "op ="
val dest_imp = dest_binop "op -->"
val dest_conj = dest_binop "op &"
--- a/src/HOL/Tools/TFL/rules.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/TFL/rules.ML Thu Jun 10 12:24:03 2010 +0200
@@ -591,11 +591,11 @@
local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
fun mk_fst tm =
- let val ty as Type("*", [fty,sty]) = type_of tm
- in Const ("fst", ty --> fty) $ tm end
+ let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
+ in Const ("Product_Type.fst", ty --> fty) $ tm end
fun mk_snd tm =
- let val ty as Type("*", [fty,sty]) = type_of tm
- in Const ("snd", ty --> sty) $ tm end
+ let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
+ in Const ("Product_Type.snd", ty --> sty) $ tm end
in
fun XFILL tych x vstruct =
let fun traverse p xocc L =
--- a/src/HOL/Tools/TFL/usyntax.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/TFL/usyntax.ML Thu Jun 10 12:24:03 2010 +0200
@@ -197,7 +197,7 @@
local
fun mk_uncurry (xt, yt, zt) =
Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
in
@@ -268,11 +268,11 @@
fun mk_pair{fst,snd} =
let val ty1 = type_of fst
val ty2 = type_of snd
- val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
+ val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
in list_comb(c,[fst,snd])
end;
-fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
+fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
| dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
@@ -372,7 +372,7 @@
(* Miscellaneous *)
fun mk_vstruct ty V =
- let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
+ let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs =
let val (ltm,vs1) = follow_prod_type ty1 vs
val (rtm,vs2) = follow_prod_type ty2 vs1
in (mk_pair{fst=ltm, snd=rtm}, vs2) end
@@ -393,7 +393,7 @@
fun dest_relation tm =
if (type_of tm = HOLogic.boolT)
- then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
+ then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
in (R,y,x)
end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
else raise USYN_ERR "dest_relation" "not a boolean term";
--- a/src/HOL/Tools/float_arith.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/float_arith.ML Thu Jun 10 12:24:03 2010 +0200
@@ -206,7 +206,7 @@
fun mk_float (a, b) = @{term "float"} $
HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
-fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
+fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
pairself (snd o HOLogic.dest_number) (a, b)
| dest_float t = ((snd o HOLogic.dest_number) t, 0);
--- a/src/HOL/Tools/refute.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Tools/refute.ML Thu Jun 10 12:24:03 2010 +0200
@@ -3050,7 +3050,7 @@
fun Product_Type_fst_interpreter thy model args t =
case t of
- Const (@{const_name fst}, Type ("fun", [Type ("*", [T, U]), _])) =>
+ Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
let
val constants_T = make_constants thy model T
val size_U = size_of_type thy model U
@@ -3069,7 +3069,7 @@
fun Product_Type_snd_interpreter thy model args t =
case t of
- Const (@{const_name snd}, Type ("fun", [Type ("*", [T, U]), _])) =>
+ Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
let
val size_T = size_of_type thy model T
val constants_U = make_constants thy model U
@@ -3279,8 +3279,8 @@
add_interpreter "lfp" lfp_interpreter #>
add_interpreter "gfp" gfp_interpreter #>
*)
- add_interpreter "fst" Product_Type_fst_interpreter #>
- add_interpreter "snd" Product_Type_snd_interpreter #>
+ add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #>
+ add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #>
add_printer "stlc" stlc_printer #>
add_printer "IDT" IDT_printer;
--- a/src/HOL/Transitive_Closure.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOL/Transitive_Closure.thy Thu Jun 10 12:24:03 2010 +0200
@@ -858,7 +858,7 @@
val rtrancl_trans = @{thm rtrancl_trans};
fun decomp (@{const Trueprop} $ t) =
- let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
+ let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
| decr (Const ("Transitive_Closure.trancl", _ ) $ r) = (r,"r+")
| decr r = (r,"r");
--- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy Thu Jun 10 12:24:03 2010 +0200
@@ -34,9 +34,9 @@
exception malformed;
-fun fst_type (Type("*",[a,_])) = a |
+fun fst_type (Type(@{type_name "*"},[a,_])) = a |
fst_type _ = raise malformed;
-fun snd_type (Type("*",[_,a])) = a |
+fun snd_type (Type(@{type_name "*"},[_,a])) = a |
snd_type _ = raise malformed;
fun element_type (Type("set",[a])) = a |
@@ -121,10 +121,10 @@
fun delete_ul_string s = implode(delete_ul (explode s));
-fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
+fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
-fun structured_tuple l (Type("*",s::t::_)) =
+fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
let
val (r,str) = structured_tuple l s;
in
--- a/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOLCF/IOA/meta_theory/automaton.ML Thu Jun 10 12:24:03 2010 +0200
@@ -298,7 +298,7 @@
(string_of_typ thy t));
fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
-comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
+comp_st_type_of thy (a::r) = Type(@{type_name "*"},[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
comp_st_type_of _ _ = error "empty automaton list";
(* checking consistency of action types (for composition) *)
@@ -387,11 +387,11 @@
thy
|> Sign.add_consts_i
[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+Type(@{type_name "*"},
+[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type(@{type_name "*"},[Type("set",[st_typ]),
+ Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
+ Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
@@ -442,11 +442,11 @@
thy
|> Sign.add_consts_i
[(Binding.name automaton_name,
-Type("*",
-[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
- Type("*",[Type("set",[st_typ]),
- Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
- Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
+Type(@{type_name "*"},
+[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
+ Type(@{type_name "*"},[Type("set",[st_typ]),
+ Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
+ Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
,NoSyn)]
|> add_defs
[(automaton_name ^ "_def",
--- a/src/HOLCF/Tools/Domain/domain_library.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_library.ML Thu Jun 10 12:24:03 2010 +0200
@@ -215,7 +215,7 @@
| prj _ _ _ [] _ = raise Fail "Domain_Library.prj: empty list"
| prj f1 _ x (_::y::ys) 0 = f1 x y
| prj f1 f2 x (y:: ys) j = prj f1 f2 (f2 x y) ys (j-1);
-fun proj x = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
+fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x;
fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
val UU = %%: @{const_name UU};
--- a/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jun 10 12:24:02 2010 +0200
+++ b/src/HOLCF/Tools/Domain/domain_theorems.ML Thu Jun 10 12:24:03 2010 +0200
@@ -179,7 +179,7 @@
then copy_of_dtyp map_tab
mk_take (dtyp_of arg) ` (%# arg)
else (%# arg);
- val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
+ val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
val rhs = con_app2 con one_rhs args;
val goal = mk_trp (lhs === rhs);
val rules =