src/HOL/Tools/Quotient/quotient_term.ML
changeset 38558 32ad17fe2b9c
parent 37744 3daaf23b9ab4
child 38624 9bb0016f7e60
     1.1 --- a/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:54 2010 +0200
     1.2 +++ b/src/HOL/Tools/Quotient/quotient_term.ML	Thu Aug 19 16:08:59 2010 +0200
     1.3 @@ -490,16 +490,16 @@
     1.4           else mk_bex1_rel $ resrel $ subtrm
     1.5         end
     1.6  
     1.7 -  | (Const (@{const_name "Ex1"}, ty) $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
     1.8 +  | (Const (@{const_name Ex1}, ty) $ t, Const (@{const_name Ex1}, ty') $ t') =>
     1.9         let
    1.10           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.11         in
    1.12 -         if ty = ty' then Const (@{const_name "Ex1"}, ty) $ subtrm
    1.13 +         if ty = ty' then Const (@{const_name Ex1}, ty) $ subtrm
    1.14           else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
    1.15         end
    1.16  
    1.17    | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
    1.18 -     Const (@{const_name "All"}, ty') $ t') =>
    1.19 +     Const (@{const_name All}, ty') $ t') =>
    1.20         let
    1.21           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.22           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
    1.23 @@ -510,7 +510,7 @@
    1.24         end
    1.25  
    1.26    | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
    1.27 -     Const (@{const_name "Ex"}, ty') $ t') =>
    1.28 +     Const (@{const_name Ex}, ty') $ t') =>
    1.29         let
    1.30           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.31           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
    1.32 @@ -520,7 +520,7 @@
    1.33           else mk_bex $ (mk_resp $ resrel) $ subtrm
    1.34         end
    1.35  
    1.36 -  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name "Ex1"}, ty') $ t') =>
    1.37 +  | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
    1.38         let
    1.39           val subtrm = apply_subt (regularize_trm ctxt) (t, t')
    1.40           val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
    1.41 @@ -638,10 +638,10 @@
    1.42     as the type of subterms needs to be calculated   *)
    1.43  fun inj_repabs_trm ctxt (rtrm, qtrm) =
    1.44   case (rtrm, qtrm) of
    1.45 -    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name "All"}, _) $ t') =>
    1.46 +    (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
    1.47         Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.48  
    1.49 -  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name "Ex"}, _) $ t') =>
    1.50 +  | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
    1.51         Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
    1.52  
    1.53    | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>