tuned quotes, antiquotations and whitespace
authorhaftmann
Thu Jun 10 12:24:03 2010 +0200 (2010-06-10)
changeset 37391476270a6c2dc
parent 37390 8781d80026fc
child 37392 b39f640b94d4
tuned quotes, antiquotations and whitespace
src/HOL/Decision_Procs/Approximation.thy
src/HOL/Hoare/hoare_tac.ML
src/HOL/Import/Generate-HOL/GenHOL4Base.thy
src/HOL/Import/Generate-HOLLight/GenHOLLight.thy
src/HOL/Import/HOL/pair.imp
src/HOL/Import/HOLLight/hollight.imp
src/HOL/Modelcheck/mucke_oracle.ML
src/HOL/Nominal/nominal_atoms.ML
src/HOL/Nominal/nominal_datatype.ML
src/HOL/Nominal/nominal_permeq.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Tools/Function/function_lib.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/TFL/dcterm.ML
src/HOL/Tools/TFL/rules.ML
src/HOL/Tools/TFL/usyntax.ML
src/HOL/Tools/float_arith.ML
src/HOL/Tools/refute.ML
src/HOL/Transitive_Closure.thy
src/HOLCF/IOA/Modelcheck/MuIOA.thy
src/HOLCF/IOA/meta_theory/automaton.ML
src/HOLCF/Tools/Domain/domain_library.ML
src/HOLCF/Tools/Domain/domain_theorems.ML
     1.1 --- a/src/HOL/Decision_Procs/Approximation.thy	Thu Jun 10 12:24:02 2010 +0200
     1.2 +++ b/src/HOL/Decision_Procs/Approximation.thy	Thu Jun 10 12:24:03 2010 +0200
     1.3 @@ -3440,7 +3440,7 @@
     1.4  
     1.5    fun dest_float (@{const "Float"} $ m $ e) = (snd (HOLogic.dest_number m), snd (HOLogic.dest_number e))
     1.6    fun dest_ivl (Const (@{const_name "Some"}, _) $
     1.7 -                (Const (@{const_name "Pair"}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
     1.8 +                (Const (@{const_name Pair}, _) $ u $ l)) = SOME (dest_float u, dest_float l)
     1.9      | dest_ivl (Const (@{const_name "None"}, _)) = NONE
    1.10      | dest_ivl t = raise TERM ("dest_result", [t])
    1.11  
     2.1 --- a/src/HOL/Hoare/hoare_tac.ML	Thu Jun 10 12:24:02 2010 +0200
     2.2 +++ b/src/HOL/Hoare/hoare_tac.ML	Thu Jun 10 12:24:03 2010 +0200
     2.3 @@ -41,9 +41,9 @@
     2.4                 else let val (n, T) = dest_Free x ;
     2.5                          val z = mk_bodyC xs;
     2.6                          val T2 = case z of Free(_, T) => T
     2.7 -                                         | Const ("Pair", Type ("fun", [_, Type
     2.8 +                                         | Const (@{const_name Pair}, Type ("fun", [_, Type
     2.9                                              ("fun", [_, T])])) $ _ $ _ => T;
    2.10 -                 in Const ("Pair", [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    2.11 +                 in Const (@{const_name Pair}, [T, T2] ---> mk_prodT (T, T2)) $ x $ z end;
    2.12  
    2.13  (** maps a subgoal of the form:
    2.14          VARS x1 ... xn {._.} _ {._.} or to [x1,...,xn]**)
     3.1 --- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jun 10 12:24:02 2010 +0200
     3.2 +++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Thu Jun 10 12:24:03 2010 +0200
     3.3 @@ -123,7 +123,7 @@
     3.4  import_theory pair;
     3.5  
     3.6  type_maps
     3.7 -    prod > "*";
     3.8 +    prod > "Product_Type.*";
     3.9  
    3.10  const_maps
    3.11      ","       > Pair
     4.1 --- a/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jun 10 12:24:02 2010 +0200
     4.2 +++ b/src/HOL/Import/Generate-HOLLight/GenHOLLight.thy	Thu Jun 10 12:24:03 2010 +0200
     4.3 @@ -38,9 +38,9 @@
     4.4    bool > bool
     4.5    fun > fun
     4.6    N_1 >  Product_Type.unit
     4.7 -  prod > "*"
     4.8 -  num > nat
     4.9 -  sum > "+"
    4.10 +  prod > "Product_Type.*"
    4.11 +  num > Nat.nat
    4.12 +  sum > "Sum_Type.+"
    4.13  (*  option > Datatype.option*);
    4.14  
    4.15  const_renames
     5.1 --- a/src/HOL/Import/HOL/pair.imp	Thu Jun 10 12:24:02 2010 +0200
     5.2 +++ b/src/HOL/Import/HOL/pair.imp	Thu Jun 10 12:24:03 2010 +0200
     5.3 @@ -7,17 +7,17 @@
     5.4    "LEX" > "LEX_def"
     5.5  
     5.6  type_maps
     5.7 -  "prod" > "*"
     5.8 +  "prod" > "Product_Type.*"
     5.9  
    5.10  const_maps
    5.11 -  "pair_case" > "split"
    5.12 -  "UNCURRY" > "split"
    5.13 -  "SND" > "snd"
    5.14 +  "pair_case" > "Product_Type.split"
    5.15 +  "UNCURRY" > "Product_Type.split"
    5.16 +  "FST" > "Product_Type.fst"
    5.17 +  "SND" > "Product_Type.snd"
    5.18    "RPROD" > "HOL4Base.pair.RPROD"
    5.19    "LEX" > "HOL4Base.pair.LEX"
    5.20 -  "FST" > "fst"
    5.21    "CURRY" > "Product_Type.curry"
    5.22 -  "," > "Pair"
    5.23 +  "," > "Product_Type.Pair"
    5.24    "##" > "prod_fun"
    5.25  
    5.26  thm_maps
     6.1 --- a/src/HOL/Import/HOLLight/hollight.imp	Thu Jun 10 12:24:02 2010 +0200
     6.2 +++ b/src/HOL/Import/HOLLight/hollight.imp	Thu Jun 10 12:24:03 2010 +0200
     6.3 @@ -6,7 +6,7 @@
     6.4    "sum" > "+"
     6.5    "recspace" > "HOLLight.hollight.recspace"
     6.6    "real" > "HOLLight.hollight.real"
     6.7 -  "prod" > "*"
     6.8 +  "prod" > "Product_Type.*"
     6.9    "option" > "HOLLight.hollight.option"
    6.10    "num" > "Nat.nat"
    6.11    "nadd" > "HOLLight.hollight.nadd"
    6.12 @@ -131,7 +131,7 @@
    6.13    "SUC" > "Nat.Suc"
    6.14    "SUBSET" > "HOLLight.hollight.SUBSET"
    6.15    "SOME" > "HOLLight.hollight.SOME"
    6.16 -  "SND" > "snd"
    6.17 +  "SND" > "Product_Type.snd"
    6.18    "SING" > "HOLLight.hollight.SING"
    6.19    "SETSPEC" > "HOLLight.hollight.SETSPEC"
    6.20    "REVERSE" > "HOLLight.hollight.REVERSE"
    6.21 @@ -188,7 +188,7 @@
    6.22    "GSPEC" > "HOLLight.hollight.GSPEC"
    6.23    "GEQ" > "HOLLight.hollight.GEQ"
    6.24    "GABS" > "HOLLight.hollight.GABS"
    6.25 -  "FST" > "fst"
    6.26 +  "FST" > "Product_Type.fst"
    6.27    "FNIL" > "HOLLight.hollight.FNIL"
    6.28    "FINREC" > "HOLLight.hollight.FINREC"
    6.29    "FINITE" > "HOLLight.hollight.FINITE"
    6.30 @@ -239,7 +239,7 @@
    6.31    "<" > "HOLLight.hollight.<"
    6.32    "/\\" > "op &"
    6.33    "-" > "Groups.minus" :: "nat => nat => nat"
    6.34 -  "," > "Pair"
    6.35 +  "," > "Product_Type.Pair"
    6.36    "+" > "Groups.plus" :: "nat => nat => nat"
    6.37    "*" > "Groups.times" :: "nat => nat => nat"
    6.38    "$" > "HOLLight.hollight.$"
     7.1 --- a/src/HOL/Modelcheck/mucke_oracle.ML	Thu Jun 10 12:24:02 2010 +0200
     7.2 +++ b/src/HOL/Modelcheck/mucke_oracle.ML	Thu Jun 10 12:24:03 2010 +0200
     7.3 @@ -832,7 +832,7 @@
     7.4  
     7.5  (* OUTPUT - relevant *)
     7.6  (* transforms constructor term to a mucke-suitable output *)
     7.7 -fun term_OUTPUT sg (Const("Pair",_) $ a $ b) =
     7.8 +fun term_OUTPUT sg (Const(@{const_name Pair},_) $ a $ b) =
     7.9                  (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
    7.10  term_OUTPUT sg (a $ b) = (term_OUTPUT sg a) ^ "_I_" ^ (term_OUTPUT sg b) |
    7.11  term_OUTPUT sg (Const(s,t)) = post_last_dot s |
     8.1 --- a/src/HOL/Nominal/nominal_atoms.ML	Thu Jun 10 12:24:02 2010 +0200
     8.2 +++ b/src/HOL/Nominal/nominal_atoms.ML	Thu Jun 10 12:24:03 2010 +0200
     8.3 @@ -543,7 +543,7 @@
     8.4          |> AxClass.prove_arity ("Nominal.noption",[[cls_name]],[cls_name]) (pt_proof pt_thm_noptn) 
     8.5          |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (pt_proof pt_thm_optn)
     8.6          |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (pt_proof pt_thm_list)
     8.7 -        |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
     8.8 +        |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (pt_proof pt_thm_prod)
     8.9          |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    8.10                                      (pt_proof pt_thm_nprod)
    8.11          |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (pt_proof pt_thm_unit)
    8.12 @@ -604,7 +604,7 @@
    8.13          in 
    8.14           thy
    8.15           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (fs_proof fs_thm_unit) 
    8.16 -         |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    8.17 +         |> AxClass.prove_arity (@{type_name "*"},[[cls_name],[cls_name]],[cls_name]) (fs_proof fs_thm_prod) 
    8.18           |> AxClass.prove_arity ("Nominal.nprod",[[cls_name],[cls_name]],[cls_name]) 
    8.19                                       (fs_proof fs_thm_nprod) 
    8.20           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (fs_proof fs_thm_list)
    8.21 @@ -686,7 +686,7 @@
    8.22          in
    8.23           thy'
    8.24           |> AxClass.prove_arity ("Product_Type.unit",[],[cls_name]) (cp_proof cp_thm_unit)
    8.25 -         |> AxClass.prove_arity ("*",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    8.26 +         |> AxClass.prove_arity (@{type_name "*"}, [[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_prod)
    8.27           |> AxClass.prove_arity ("List.list",[[cls_name]],[cls_name]) (cp_proof cp_thm_list)
    8.28           |> AxClass.prove_arity ("fun",[[cls_name],[cls_name]],[cls_name]) (cp_proof cp_thm_fun)
    8.29           |> AxClass.prove_arity ("Option.option",[[cls_name]],[cls_name]) (cp_proof cp_thm_optn)
     9.1 --- a/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 10 12:24:02 2010 +0200
     9.2 +++ b/src/HOL/Nominal/nominal_datatype.ML	Thu Jun 10 12:24:03 2010 +0200
     9.3 @@ -121,7 +121,7 @@
     9.4  
     9.5  val dj_cp = thm "dj_cp";
     9.6  
     9.7 -fun dest_permT (Type ("fun", [Type ("List.list", [Type ("*", [T, _])]),
     9.8 +fun dest_permT (Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [T, _])]),
     9.9        Type ("fun", [_, U])])) = (T, U);
    9.10  
    9.11  fun permTs_of (Const ("Nominal.perm", T) $ t $ u) = fst (dest_permT T) :: permTs_of u
    10.1 --- a/src/HOL/Nominal/nominal_permeq.ML	Thu Jun 10 12:24:02 2010 +0200
    10.2 +++ b/src/HOL/Nominal/nominal_permeq.ML	Thu Jun 10 12:24:03 2010 +0200
    10.3 @@ -103,7 +103,7 @@
    10.4      case redex of 
    10.5          (* case pi o (f x) == (pi o f) (pi o x)          *)
    10.6          (Const("Nominal.perm",
    10.7 -          Type("fun",[Type("List.list",[Type("*",[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    10.8 +          Type("fun",[Type("List.list",[Type(@{type_name "*"},[Type(n,_),_])]),_])) $ pi $ (f $ x)) => 
    10.9              (if (applicable_app f) then
   10.10                let
   10.11                  val name = Long_Name.base_name n
   10.12 @@ -190,8 +190,8 @@
   10.13  fun perm_compose_simproc' sg ss redex =
   10.14    (case redex of
   10.15       (Const ("Nominal.perm", Type ("fun", [Type ("List.list", 
   10.16 -       [Type ("*", [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   10.17 -         Type ("fun", [Type ("List.list", [Type ("*", [U as Type (uname,_),_])]),_])) $ 
   10.18 +       [Type (@{type_name "*"}, [T as Type (tname,_),_])]),_])) $ pi1 $ (Const ("Nominal.perm", 
   10.19 +         Type ("fun", [Type ("List.list", [Type (@{type_name "*"}, [U as Type (uname,_),_])]),_])) $ 
   10.20            pi2 $ t)) =>
   10.21      let
   10.22        val tname' = Long_Name.base_name tname
    11.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Thu Jun 10 12:24:02 2010 +0200
    11.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Thu Jun 10 12:24:03 2010 +0200
    11.3 @@ -103,7 +103,7 @@
    11.4    let fun get_pi_aux s =
    11.5          (case s of
    11.6            (Const (@{const_name "perm"} ,typrm) $
    11.7 -             (Var (pi,typi as Type(@{type_name "list"}, [Type ("*", [Type (tyatm,[]),_])]))) $
    11.8 +             (Var (pi,typi as Type(@{type_name "list"}, [Type (@{type_name "*"}, [Type (tyatm,[]),_])]))) $
    11.9                 (Var (n,ty))) =>
   11.10               let
   11.11                  (* FIXME: this should be an operation the library *)
    12.1 --- a/src/HOL/Tools/Function/function_lib.ML	Thu Jun 10 12:24:02 2010 +0200
    12.2 +++ b/src/HOL/Tools/Function/function_lib.ML	Thu Jun 10 12:24:03 2010 +0200
    12.3 @@ -24,7 +24,7 @@
    12.4    case vars of
    12.5      (Free v) => lambda (Free v) t
    12.6    | (Var v) => lambda (Var v) t
    12.7 -  | (Const ("Pair", Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
    12.8 +  | (Const (@{const_name Pair}, Type ("fun", [Ta, Type ("fun", [Tb, _])]))) $ us $ vs =>
    12.9        (HOLogic.split_const (Ta,Tb, fastype_of t)) $ (tupled_lambda us (tupled_lambda vs t))
   12.10    | _ => raise Match
   12.11  
    13.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jun 10 12:24:02 2010 +0200
    13.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jun 10 12:24:03 2010 +0200
    13.3 @@ -148,7 +148,7 @@
    13.4      val cs = Function_Lib.dest_binop_list @{const_name Lattices.sup} rel
    13.5      fun collect_pats (Const (@{const_name Collect}, _) $ Abs (_, _, c)) =
    13.6        let
    13.7 -        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ _)
    13.8 +        val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ _)
    13.9            = Term.strip_qnt_body "Ex" c
   13.10        in cons r o cons l end
   13.11    in
   13.12 @@ -185,7 +185,7 @@
   13.13      val vs = Term.strip_qnt_vars "Ex" c
   13.14  
   13.15      (* FIXME: throw error "dest_call" for malformed terms *)
   13.16 -    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const ("Pair", _) $ r $ l)) $ Gam)
   13.17 +    val (Const ("op &", _) $ (Const ("op =", _) $ _ $ (Const (@{const_name Pair}, _) $ r $ l)) $ Gam)
   13.18        = Term.strip_qnt_body "Ex" c
   13.19      val (p, l') = dest_inj sk l
   13.20      val (q, r') = dest_inj sk r
    14.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 10 12:24:02 2010 +0200
    14.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Thu Jun 10 12:24:03 2010 +0200
    14.3 @@ -265,12 +265,12 @@
    14.4  fun replace_ho_args mode hoargs ts =
    14.5    let
    14.6      fun replace (Fun _, _) (arg' :: hoargs') = (arg', hoargs')
    14.7 -      | replace (Pair (m1, m2), Const ("Pair", T) $ t1 $ t2) hoargs =
    14.8 +      | replace (Pair (m1, m2), Const (@{const_name Pair}, T) $ t1 $ t2) hoargs =
    14.9          let
   14.10            val (t1', hoargs') = replace (m1, t1) hoargs
   14.11            val (t2', hoargs'') = replace (m2, t2) hoargs'
   14.12          in
   14.13 -          (Const ("Pair", T) $ t1' $ t2', hoargs'')
   14.14 +          (Const (@{const_name Pair}, T) $ t1' $ t2', hoargs'')
   14.15          end
   14.16        | replace (_, t) hoargs = (t, hoargs)
   14.17    in
   14.18 @@ -290,7 +290,7 @@
   14.19  fun split_map_mode f mode ts =
   14.20    let
   14.21      fun split_arg_mode' (m as Fun _) t = f m t
   14.22 -      | split_arg_mode' (Pair (m1, m2)) (Const ("Pair", _) $ t1 $ t2) =
   14.23 +      | split_arg_mode' (Pair (m1, m2)) (Const (@{const_name Pair}, _) $ t1 $ t2) =
   14.24          let
   14.25            val (i1, o1) = split_arg_mode' m1 t1
   14.26            val (i2, o2) = split_arg_mode' m2 t2
   14.27 @@ -334,7 +334,7 @@
   14.28    end
   14.29    | fold_map_aterms_prodT comb f T s = f T s
   14.30  
   14.31 -fun map_filter_prod f (Const ("Pair", _) $ t1 $ t2) =
   14.32 +fun map_filter_prod f (Const (@{const_name Pair}, _) $ t1 $ t2) =
   14.33    comb_option HOLogic.mk_prod (map_filter_prod f t1, map_filter_prod f t2)
   14.34    | map_filter_prod f t = f t
   14.35  
   14.36 @@ -561,8 +561,8 @@
   14.37  
   14.38  (* combinators to apply a function to all basic parts of nested products *)
   14.39  
   14.40 -fun map_products f (Const ("Pair", T) $ t1 $ t2) =
   14.41 -  Const ("Pair", T) $ map_products f t1 $ map_products f t2
   14.42 +fun map_products f (Const (@{const_name Pair}, T) $ t1 $ t2) =
   14.43 +  Const (@{const_name Pair}, T) $ map_products f t1 $ map_products f t2
   14.44    | map_products f t = f t
   14.45  
   14.46  (* split theorems of case expressions *)
   14.47 @@ -756,7 +756,7 @@
   14.48        (case HOLogic.strip_tupleT (fastype_of arg) of
   14.49          (Ts as _ :: _ :: _) =>
   14.50          let
   14.51 -          fun rewrite_arg' (Const (@{const_name "Pair"}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
   14.52 +          fun rewrite_arg' (Const (@{const_name Pair}, _) $ _ $ t2, Type (@{type_name "*"}, [_, T2]))
   14.53              (args, (pats, intro_t, ctxt)) = rewrite_arg' (t2, T2) (args, (pats, intro_t, ctxt))
   14.54              | rewrite_arg' (t, Type (@{type_name "*"}, [T1, T2])) (args, (pats, intro_t, ctxt)) =
   14.55                let
    15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 10 12:24:02 2010 +0200
    15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Thu Jun 10 12:24:03 2010 +0200
    15.3 @@ -117,7 +117,7 @@
    15.4    end;
    15.5  
    15.6  fun dest_randomT (Type ("fun", [@{typ Random.seed},
    15.7 -  Type ("*", [Type ("*", [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    15.8 +  Type (@{type_name "*"}, [Type (@{type_name "*"}, [T, @{typ "unit => Code_Evaluation.term"}]) ,@{typ Random.seed}])])) = T
    15.9    | dest_randomT T = raise TYPE ("dest_randomT", [T], [])
   15.10  
   15.11  fun mk_tracing s t =
   15.12 @@ -467,7 +467,7 @@
   15.13  
   15.14  (* generation of case rules from user-given introduction rules *)
   15.15  
   15.16 -fun mk_args2 (Type ("*", [T1, T2])) st =
   15.17 +fun mk_args2 (Type (@{type_name "*"}, [T1, T2])) st =
   15.18      let
   15.19        val (t1, st') = mk_args2 T1 st
   15.20        val (t2, st'') = mk_args2 T2 st'
   15.21 @@ -1099,7 +1099,7 @@
   15.22  fun all_input_of T =
   15.23    let
   15.24      val (Ts, U) = strip_type T
   15.25 -    fun input_of (Type ("*", [T1, T2])) = Pair (input_of T1, input_of T2)
   15.26 +    fun input_of (Type (@{type_name "*"}, [T1, T2])) = Pair (input_of T1, input_of T2)
   15.27        | input_of _ = Input
   15.28    in
   15.29      if U = HOLogic.boolT then
   15.30 @@ -1190,7 +1190,7 @@
   15.31  
   15.32  fun missing_vars vs t = subtract (op =) vs (term_vs t)
   15.33  
   15.34 -fun output_terms (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =
   15.35 +fun output_terms (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =
   15.36      output_terms (t1, d1)  @ output_terms (t2, d2)
   15.37    | output_terms (t1 $ t2, Mode_App (d1, d2)) =
   15.38      output_terms (t1, d1)  @ output_terms (t2, d2)
   15.39 @@ -1206,7 +1206,7 @@
   15.40        SOME ms => SOME (map (fn m => (Context m , [])) ms)
   15.41      | NONE => NONE)
   15.42  
   15.43 -fun derivations_of (ctxt : Proof.context) modes vs (Const ("Pair", _) $ t1 $ t2) (Pair (m1, m2)) =
   15.44 +fun derivations_of (ctxt : Proof.context) modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) (Pair (m1, m2)) =
   15.45      map_product
   15.46        (fn (m1, mvars1) => fn (m2, mvars2) => (Mode_Pair (m1, m2), union (op =) mvars1 mvars2))
   15.47          (derivations_of ctxt modes vs t1 m1) (derivations_of ctxt modes vs t2 m2)
   15.48 @@ -1236,7 +1236,7 @@
   15.49      else if eq_mode (m, Output) then
   15.50        (if is_possible_output ctxt vs t then [(Term Output, [])] else [])
   15.51      else []
   15.52 -and all_derivations_of ctxt modes vs (Const ("Pair", _) $ t1 $ t2) =
   15.53 +and all_derivations_of ctxt modes vs (Const (@{const_name Pair}, _) $ t1 $ t2) =
   15.54    let
   15.55      val derivs1 = all_derivations_of ctxt modes vs t1
   15.56      val derivs2 = all_derivations_of ctxt modes vs t2
   15.57 @@ -1665,7 +1665,7 @@
   15.58    (case (t, deriv) of
   15.59      (t1 $ t2, Mode_App (deriv1, deriv2)) =>
   15.60        string_of_tderiv ctxt (t1, deriv1) ^ " $ " ^ string_of_tderiv ctxt (t2, deriv2)
   15.61 -  | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
   15.62 +  | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (deriv1, deriv2)) =>
   15.63      "(" ^ string_of_tderiv ctxt (t1, deriv1) ^ ", " ^ string_of_tderiv ctxt (t2, deriv2) ^ ")"
   15.64    | (t, Term Input) => Syntax.string_of_term ctxt t ^ "[Input]"
   15.65    | (t, Term Output) => Syntax.string_of_term ctxt t ^ "[Output]"
   15.66 @@ -1692,7 +1692,7 @@
   15.67            val bs = map (pair "x") (binder_types (fastype_of t))
   15.68            val bounds = map Bound (rev (0 upto (length bs) - 1))
   15.69          in SOME (list_abs (bs, mk_if compfuns (list_comb (t, bounds)))) end
   15.70 -      | (Const ("Pair", _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
   15.71 +      | (Const (@{const_name Pair}, _) $ t1 $ t2, Mode_Pair (d1, d2)) =>
   15.72          (case (expr_of (t1, d1), expr_of (t2, d2)) of
   15.73            (NONE, NONE) => NONE
   15.74          | (NONE, SOME t) => SOME t
   15.75 @@ -2010,7 +2010,7 @@
   15.76          (ks @ [SOME k]))) arities));
   15.77  
   15.78  fun split_lambda (x as Free _) t = lambda x t
   15.79 -  | split_lambda (Const ("Pair", _) $ t1 $ t2) t =
   15.80 +  | split_lambda (Const (@{const_name Pair}, _) $ t1 $ t2) t =
   15.81      HOLogic.mk_split (split_lambda t1 (split_lambda t2 t))
   15.82    | split_lambda (Const ("Product_Type.Unity", _)) t = Abs ("x", HOLogic.unitT, t)
   15.83    | split_lambda t _ = raise (TERM ("split_lambda", [t]))
   15.84 @@ -2019,7 +2019,7 @@
   15.85    | strip_split_abs (Abs (_, _, t)) = strip_split_abs t
   15.86    | strip_split_abs t = t
   15.87  
   15.88 -fun mk_args is_eval (m as Pair (m1, m2), T as Type ("*", [T1, T2])) names =
   15.89 +fun mk_args is_eval (m as Pair (m1, m2), T as Type (@{type_name "*"}, [T1, T2])) names =
   15.90      if eq_mode (m, Input) orelse eq_mode (m, Output) then
   15.91        let
   15.92          val x = Name.variant names "x"
   15.93 @@ -3112,7 +3112,7 @@
   15.94    in
   15.95      if defined_functions compilation ctxt name then
   15.96        let
   15.97 -        fun extract_mode (Const ("Pair", _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
   15.98 +        fun extract_mode (Const (@{const_name Pair}, _) $ t1 $ t2) = Pair (extract_mode t1, extract_mode t2)
   15.99            | extract_mode (Free (x, _)) = if member (op =) output_names x then Output else Input
  15.100            | extract_mode _ = Input
  15.101          val user_mode = fold_rev (curry Fun) (map extract_mode all_args) Bool
    16.1 --- a/src/HOL/Tools/TFL/dcterm.ML	Thu Jun 10 12:24:02 2010 +0200
    16.2 +++ b/src/HOL/Tools/TFL/dcterm.ML	Thu Jun 10 12:24:03 2010 +0200
    16.3 @@ -129,7 +129,7 @@
    16.4  
    16.5  
    16.6  val dest_neg    = dest_monop "not"
    16.7 -val dest_pair   = dest_binop "Pair";
    16.8 +val dest_pair   = dest_binop @{const_name Pair};
    16.9  val dest_eq     = dest_binop "op ="
   16.10  val dest_imp    = dest_binop "op -->"
   16.11  val dest_conj   = dest_binop "op &"
    17.1 --- a/src/HOL/Tools/TFL/rules.ML	Thu Jun 10 12:24:02 2010 +0200
    17.2 +++ b/src/HOL/Tools/TFL/rules.ML	Thu Jun 10 12:24:03 2010 +0200
    17.3 @@ -591,11 +591,11 @@
    17.4  
    17.5  local fun dest_pair M = let val {fst,snd} = S.dest_pair M in (fst,snd) end
    17.6        fun mk_fst tm =
    17.7 -          let val ty as Type("*", [fty,sty]) = type_of tm
    17.8 -          in  Const ("fst", ty --> fty) $ tm  end
    17.9 +          let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
   17.10 +          in  Const ("Product_Type.fst", ty --> fty) $ tm  end
   17.11        fun mk_snd tm =
   17.12 -          let val ty as Type("*", [fty,sty]) = type_of tm
   17.13 -          in  Const ("snd", ty --> sty) $ tm  end
   17.14 +          let val ty as Type("Product_Type.*", [fty,sty]) = type_of tm
   17.15 +          in  Const ("Product_Type.snd", ty --> sty) $ tm  end
   17.16  in
   17.17  fun XFILL tych x vstruct =
   17.18    let fun traverse p xocc L =
    18.1 --- a/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 10 12:24:02 2010 +0200
    18.2 +++ b/src/HOL/Tools/TFL/usyntax.ML	Thu Jun 10 12:24:03 2010 +0200
    18.3 @@ -197,7 +197,7 @@
    18.4  local
    18.5  fun mk_uncurry (xt, yt, zt) =
    18.6      Const(@{const_name split}, (xt --> yt --> zt) --> prod_ty xt yt --> zt)
    18.7 -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
    18.8 +fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
    18.9    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair"
   18.10  fun is_var (Var _) = true | is_var (Free _) = true | is_var _ = false
   18.11  in
   18.12 @@ -268,11 +268,11 @@
   18.13  fun mk_pair{fst,snd} =
   18.14     let val ty1 = type_of fst
   18.15         val ty2 = type_of snd
   18.16 -       val c = Const("Pair",ty1 --> ty2 --> prod_ty ty1 ty2)
   18.17 +       val c = Const(@{const_name Pair},ty1 --> ty2 --> prod_ty ty1 ty2)
   18.18     in list_comb(c,[fst,snd])
   18.19     end;
   18.20  
   18.21 -fun dest_pair(Const("Pair",_) $ M $ N) = {fst=M, snd=N}
   18.22 +fun dest_pair(Const(@{const_name Pair},_) $ M $ N) = {fst=M, snd=N}
   18.23    | dest_pair _ = raise USYN_ERR "dest_pair" "not a pair";
   18.24  
   18.25  
   18.26 @@ -372,7 +372,7 @@
   18.27  (* Miscellaneous *)
   18.28  
   18.29  fun mk_vstruct ty V =
   18.30 -  let fun follow_prod_type (Type("*",[ty1,ty2])) vs =
   18.31 +  let fun follow_prod_type (Type(@{type_name "*"},[ty1,ty2])) vs =
   18.32                let val (ltm,vs1) = follow_prod_type ty1 vs
   18.33                    val (rtm,vs2) = follow_prod_type ty2 vs1
   18.34                in (mk_pair{fst=ltm, snd=rtm}, vs2) end
   18.35 @@ -393,7 +393,7 @@
   18.36  
   18.37  fun dest_relation tm =
   18.38     if (type_of tm = HOLogic.boolT)
   18.39 -   then let val (Const("op :",_) $ (Const("Pair",_)$y$x) $ R) = tm
   18.40 +   then let val (Const("op :",_) $ (Const(@{const_name Pair},_)$y$x) $ R) = tm
   18.41          in (R,y,x)
   18.42          end handle Bind => raise USYN_ERR "dest_relation" "unexpected term structure"
   18.43     else raise USYN_ERR "dest_relation" "not a boolean term";
    19.1 --- a/src/HOL/Tools/float_arith.ML	Thu Jun 10 12:24:02 2010 +0200
    19.2 +++ b/src/HOL/Tools/float_arith.ML	Thu Jun 10 12:24:03 2010 +0200
    19.3 @@ -206,7 +206,7 @@
    19.4  fun mk_float (a, b) = @{term "float"} $
    19.5    HOLogic.mk_prod (pairself (HOLogic.mk_number HOLogic.intT) (a, b));
    19.6  
    19.7 -fun dest_float (Const ("Float.float", _) $ (Const ("Pair", _) $ a $ b)) =
    19.8 +fun dest_float (Const ("Float.float", _) $ (Const (@{const_name Pair}, _) $ a $ b)) =
    19.9        pairself (snd o HOLogic.dest_number) (a, b)
   19.10    | dest_float t = ((snd o HOLogic.dest_number) t, 0);
   19.11  
    20.1 --- a/src/HOL/Tools/refute.ML	Thu Jun 10 12:24:02 2010 +0200
    20.2 +++ b/src/HOL/Tools/refute.ML	Thu Jun 10 12:24:03 2010 +0200
    20.3 @@ -3050,7 +3050,7 @@
    20.4  
    20.5    fun Product_Type_fst_interpreter thy model args t =
    20.6      case t of
    20.7 -      Const (@{const_name fst}, Type ("fun", [Type ("*", [T, U]), _])) =>
    20.8 +      Const (@{const_name fst}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
    20.9        let
   20.10          val constants_T = make_constants thy model T
   20.11          val size_U      = size_of_type thy model U
   20.12 @@ -3069,7 +3069,7 @@
   20.13  
   20.14    fun Product_Type_snd_interpreter thy model args t =
   20.15      case t of
   20.16 -      Const (@{const_name snd}, Type ("fun", [Type ("*", [T, U]), _])) =>
   20.17 +      Const (@{const_name snd}, Type ("fun", [Type (@{type_name "*"}, [T, U]), _])) =>
   20.18        let
   20.19          val size_T      = size_of_type thy model T
   20.20          val constants_U = make_constants thy model U
   20.21 @@ -3279,8 +3279,8 @@
   20.22       add_interpreter "lfp" lfp_interpreter #>
   20.23       add_interpreter "gfp" gfp_interpreter #>
   20.24  *)
   20.25 -     add_interpreter "fst" Product_Type_fst_interpreter #>
   20.26 -     add_interpreter "snd" Product_Type_snd_interpreter #>
   20.27 +     add_interpreter "Product_Type.fst" Product_Type_fst_interpreter #>
   20.28 +     add_interpreter "Product_Type.snd" Product_Type_snd_interpreter #>
   20.29       add_printer "stlc" stlc_printer #>
   20.30       add_printer "IDT"  IDT_printer;
   20.31  
    21.1 --- a/src/HOL/Transitive_Closure.thy	Thu Jun 10 12:24:02 2010 +0200
    21.2 +++ b/src/HOL/Transitive_Closure.thy	Thu Jun 10 12:24:03 2010 +0200
    21.3 @@ -858,7 +858,7 @@
    21.4    val rtrancl_trans = @{thm rtrancl_trans};
    21.5  
    21.6    fun decomp (@{const Trueprop} $ t) =
    21.7 -    let fun dec (Const ("op :", _) $ (Const ("Pair", _) $ a $ b) $ rel ) =
    21.8 +    let fun dec (Const ("op :", _) $ (Const (@{const_name Pair}, _) $ a $ b) $ rel ) =
    21.9          let fun decr (Const ("Transitive_Closure.rtrancl", _ ) $ r) = (r,"r*")
   21.10                | decr (Const ("Transitive_Closure.trancl", _ ) $ r)  = (r,"r+")
   21.11                | decr r = (r,"r");
    22.1 --- a/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jun 10 12:24:02 2010 +0200
    22.2 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.thy	Thu Jun 10 12:24:03 2010 +0200
    22.3 @@ -34,9 +34,9 @@
    22.4  
    22.5  exception malformed;
    22.6  
    22.7 -fun fst_type (Type("*",[a,_])) = a |
    22.8 +fun fst_type (Type(@{type_name "*"},[a,_])) = a |
    22.9  fst_type _ = raise malformed; 
   22.10 -fun snd_type (Type("*",[_,a])) = a |
   22.11 +fun snd_type (Type(@{type_name "*"},[_,a])) = a |
   22.12  snd_type _ = raise malformed;
   22.13  
   22.14  fun element_type (Type("set",[a])) = a |
   22.15 @@ -121,10 +121,10 @@
   22.16  
   22.17  fun delete_ul_string s = implode(delete_ul (explode s));
   22.18  
   22.19 -fun type_list_of sign (Type("*",a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   22.20 +fun type_list_of sign (Type(@{type_name "*"},a::b::_)) = (type_list_of sign a) @ (type_list_of sign b) |
   22.21  type_list_of sign a = [(Syntax.string_of_typ_global sign a)];
   22.22  
   22.23 -fun structured_tuple l (Type("*",s::t::_)) =
   22.24 +fun structured_tuple l (Type(@{type_name "*"},s::t::_)) =
   22.25  let
   22.26  val (r,str) = structured_tuple l s;
   22.27  in
    23.1 --- a/src/HOLCF/IOA/meta_theory/automaton.ML	Thu Jun 10 12:24:02 2010 +0200
    23.2 +++ b/src/HOLCF/IOA/meta_theory/automaton.ML	Thu Jun 10 12:24:03 2010 +0200
    23.3 @@ -298,7 +298,7 @@
    23.4  (string_of_typ thy t));
    23.5  
    23.6  fun comp_st_type_of thy [a] = st_type_of thy (aut_type_of thy a) |
    23.7 -comp_st_type_of thy (a::r) = Type("*",[st_type_of thy (aut_type_of thy a), comp_st_type_of thy r]) |
    23.8 +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]) |
    23.9  comp_st_type_of _ _ = error "empty automaton list";
   23.10  
   23.11  (* checking consistency of action types (for composition) *)
   23.12 @@ -387,11 +387,11 @@
   23.13  thy
   23.14  |> Sign.add_consts_i
   23.15  [(Binding.name automaton_name,
   23.16 -Type("*",
   23.17 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   23.18 - Type("*",[Type("set",[st_typ]),
   23.19 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   23.20 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   23.21 +Type(@{type_name "*"},
   23.22 +[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
   23.23 + Type(@{type_name "*"},[Type("set",[st_typ]),
   23.24 +  Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
   23.25 +   Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   23.26  ,NoSyn)]
   23.27  |> add_defs
   23.28  [(automaton_name ^ "_def",
   23.29 @@ -442,11 +442,11 @@
   23.30  thy
   23.31  |> Sign.add_consts_i
   23.32  [(Binding.name automaton_name,
   23.33 -Type("*",
   23.34 -[Type("*",[Type("set",[acttyp]),Type("*",[Type("set",[acttyp]),Type("set",[acttyp])])]),
   23.35 - Type("*",[Type("set",[st_typ]),
   23.36 -  Type("*",[Type("set",[Type("*",[st_typ,Type("*",[acttyp,st_typ])])]),
   23.37 -   Type("*",[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   23.38 +Type(@{type_name "*"},
   23.39 +[Type(@{type_name "*"},[Type("set",[acttyp]),Type(@{type_name "*"},[Type("set",[acttyp]),Type("set",[acttyp])])]),
   23.40 + Type(@{type_name "*"},[Type("set",[st_typ]),
   23.41 +  Type(@{type_name "*"},[Type("set",[Type(@{type_name "*"},[st_typ,Type(@{type_name "*"},[acttyp,st_typ])])]),
   23.42 +   Type(@{type_name "*"},[Type("set",[Type("set",[acttyp])]),Type("set",[Type("set",[acttyp])])])])])])
   23.43  ,NoSyn)]
   23.44  |> add_defs
   23.45  [(automaton_name ^ "_def",
    24.1 --- a/src/HOLCF/Tools/Domain/domain_library.ML	Thu Jun 10 12:24:02 2010 +0200
    24.2 +++ b/src/HOLCF/Tools/Domain/domain_library.ML	Thu Jun 10 12:24:03 2010 +0200
    24.3 @@ -215,7 +215,7 @@
    24.4    | prj _  _  _ []         _ = raise Fail "Domain_Library.prj: empty list"
    24.5    | prj f1 _  x (_::y::ys) 0 = f1 x y
    24.6    | prj f1 f2 x (y::   ys) j = prj f1 f2 (f2 x y) ys (j-1);
    24.7 -fun  proj x      = prj (fn S => K(%%:"fst" $S)) (fn S => K(%%:"snd" $S)) x;
    24.8 +fun proj x = prj (fn S => K (%%: @{const_name fst} $ S)) (fn S => K (%%: @{const_name snd} $ S)) x;
    24.9  fun lift tfn = Library.foldr (fn (x,t)=> (mk_trp(tfn x) ===> t));
   24.10  
   24.11  val UU = %%: @{const_name UU};
    25.1 --- a/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jun 10 12:24:02 2010 +0200
    25.2 +++ b/src/HOLCF/Tools/Domain/domain_theorems.ML	Thu Jun 10 12:24:03 2010 +0200
    25.3 @@ -179,7 +179,7 @@
    25.4            then copy_of_dtyp map_tab
    25.5                   mk_take (dtyp_of arg) ` (%# arg)
    25.6            else (%# arg);
    25.7 -      val lhs = (dc_take dname $ (%%:"Suc" $ %:"n"))`(con_app con args);
    25.8 +      val lhs = (dc_take dname $ (%%: @{const_name Suc} $ %:"n")) ` (con_app con args);
    25.9        val rhs = con_app2 con one_rhs args;
   25.10        val goal = mk_trp (lhs === rhs);
   25.11        val rules =