# HG changeset patch # User haftmann # Date 1276165443 -7200 # Node ID 476270a6c2dce0866b4cb3f6e5cac7f1450deceb # Parent 8781d80026fc5a6ddf7e263ded702e6fe312889f tuned quotes, antiquotations and whitespace diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Decision_Procs/Approximation.thy --- 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]) diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Hoare/hoare_tac.ML --- 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]**) diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Import/Generate-HOL/GenHOL4Base.thy --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Import/Generate-HOLLight/GenHOLLight.thy --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Import/HOL/pair.imp --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Import/HOLLight/hollight.imp --- 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.$" diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Modelcheck/mucke_oracle.ML --- 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 | diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Nominal/nominal_atoms.ML --- 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) diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Nominal/nominal_datatype.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Nominal/nominal_permeq.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Nominal/nominal_thmdecls.ML --- 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 *) diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/Function/function_lib.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/Function/termination.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/TFL/dcterm.ML --- 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 &" diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/TFL/rules.ML --- 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 = diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/TFL/usyntax.ML --- 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"; diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/float_arith.ML --- 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); diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Tools/refute.ML --- 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; diff -r 8781d80026fc -r 476270a6c2dc src/HOL/Transitive_Closure.thy --- 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"); diff -r 8781d80026fc -r 476270a6c2dc src/HOLCF/IOA/Modelcheck/MuIOA.thy --- 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 diff -r 8781d80026fc -r 476270a6c2dc src/HOLCF/IOA/meta_theory/automaton.ML --- 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", diff -r 8781d80026fc -r 476270a6c2dc src/HOLCF/Tools/Domain/domain_library.ML --- 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}; diff -r 8781d80026fc -r 476270a6c2dc src/HOLCF/Tools/Domain/domain_theorems.ML --- 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 =