--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Aug 20 20:29:50 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Sun Aug 22 10:45:53 2010 +0800
@@ -92,7 +92,7 @@
fun lift_raw_const qtys (qconst_name, rconst, mx) ctxt =
let
val rty = fastype_of rconst
- val qty = derive_qtyp qtys rty ctxt
+ val qty = derive_qtyp ctxt qtys rty
val lhs = Free (qconst_name, qty)
in
quotient_def ((NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML Fri Aug 20 20:29:50 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML Sun Aug 22 10:45:53 2010 +0800
@@ -18,7 +18,7 @@
val lift_procedure_tac: Proof.context -> thm -> int -> tactic
val lift_tac: Proof.context -> thm list -> int -> tactic
- val lifted: typ list -> Proof.context -> thm -> thm
+ val lifted: Proof.context -> typ list -> thm -> thm
val lifted_attrib: attribute
end;
@@ -627,7 +627,7 @@
THEN' SUBGOAL (fn (goal, i) =>
let
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
- val rtrm = derive_rtrm qtys goal ctxt
+ val rtrm = derive_rtrm ctxt qtys goal
val rule = procedure_inst ctxt rtrm goal
in
rtac rule i
@@ -674,15 +674,15 @@
end
-(** lifting as attribute **)
+(** lifting as an attribute **)
-fun lifted qtys ctxt thm =
+fun lifted ctxt qtys thm =
let
(* When the theorem is atomized, eta redexes are contracted,
so we do it both in the original theorem *)
val thm' = Drule.eta_contraction_rule thm
val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
- val goal = derive_qtrm qtys (prop_of thm'') ctxt'
+ val goal = derive_qtrm ctxt qtys (prop_of thm'')
in
Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
|> singleton (ProofContext.export ctxt' ctxt)
@@ -693,7 +693,7 @@
val ctxt = Context.proof_of context
val qtys = map #qtyp (Quotient_Info.quotdata_dest ctxt)
in
- lifted qtys ctxt
+ lifted ctxt qtys
end)
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_term.ML Fri Aug 20 20:29:50 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_term.ML Sun Aug 22 10:45:53 2010 +0800
@@ -26,10 +26,10 @@
val inj_repabs_trm: Proof.context -> term * term -> term
val inj_repabs_trm_chk: Proof.context -> term * term -> term
- val derive_qtyp: typ list -> typ -> Proof.context -> typ
- val derive_qtrm: typ list -> term -> Proof.context -> term
- val derive_rtyp: typ list -> typ -> Proof.context -> typ
- val derive_rtrm: typ list -> term -> Proof.context -> term
+ val derive_qtyp: Proof.context -> typ list -> typ -> typ
+ val derive_qtrm: Proof.context -> typ list -> term -> term
+ val derive_rtyp: Proof.context -> typ list -> typ -> typ
+ val derive_rtrm: Proof.context -> typ list -> term -> term
end;
structure Quotient_Term: QUOTIENT_TERM =
@@ -498,7 +498,7 @@
else mk_bex1_rel $ (equiv_relation ctxt (qnt_typ ty, qnt_typ ty')) $ subtrm
end
- | (Const (@{const_name "Ball"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name Ball}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name All}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -509,7 +509,7 @@
else mk_ball $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex"}, ty) $ (Const (@{const_name "Respects"}, _) $ resrel) $ t,
+ | (Const (@{const_name Bex}, ty) $ (Const (@{const_name Respects}, _) $ resrel) $ t,
Const (@{const_name Ex}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
@@ -520,7 +520,7 @@
else mk_bex $ (mk_resp $ resrel) $ subtrm
end
- | (Const (@{const_name "Bex1_rel"}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
+ | (Const (@{const_name Bex1_rel}, ty) $ resrel $ t, Const (@{const_name Ex1}, ty') $ t') =>
let
val subtrm = apply_subt (regularize_trm ctxt) (t, t')
val needrel = equiv_relation_chk ctxt (qnt_typ ty, qnt_typ ty')
@@ -638,18 +638,18 @@
as the type of subterms needs to be calculated *)
fun inj_repabs_trm ctxt (rtrm, qtrm) =
case (rtrm, qtrm) of
- (Const (@{const_name "Ball"}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
- Const (@{const_name "Ball"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
+ (Const (@{const_name Ball}, T) $ r $ t, Const (@{const_name All}, _) $ t') =>
+ Const (@{const_name Ball}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Bex"}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
- Const (@{const_name "Bex"}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
+ | (Const (@{const_name Bex}, T) $ r $ t, Const (@{const_name Ex}, _) $ t') =>
+ Const (@{const_name Bex}, T) $ r $ (inj_repabs_trm ctxt (t, t'))
- | (Const (@{const_name "Babs"}, T) $ r $ t, t' as (Abs _)) =>
+ | (Const (@{const_name Babs}, T) $ r $ t, t' as (Abs _)) =>
let
val rty = fastype_of rtrm
val qty = fastype_of qtrm
in
- mk_repabs ctxt (rty, qty) (Const (@{const_name "Babs"}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
+ mk_repabs ctxt (rty, qty) (Const (@{const_name Babs}, T) $ r $ (inj_repabs_trm ctxt (t, t')))
end
| (Abs (x, T, t), Abs (x', T', t')) =>
@@ -767,19 +767,19 @@
(* derives a qtyp and qtrm out of a rtyp and rtrm,
respectively
*)
-fun derive_qtyp qtys rty ctxt =
+fun derive_qtyp ctxt qtys rty =
subst_typ ctxt (mk_ty_subst qtys false ctxt) rty
-fun derive_qtrm qtys rtrm ctxt =
+fun derive_qtrm ctxt qtys rtrm =
subst_trm ctxt (mk_ty_subst qtys false ctxt) (mk_trm_subst qtys false ctxt) rtrm
(* derives a rtyp and rtrm out of a qtyp and qtrm,
respectively
*)
-fun derive_rtyp qtys qty ctxt =
+fun derive_rtyp ctxt qtys qty =
subst_typ ctxt (mk_ty_subst qtys true ctxt) qty
-fun derive_rtrm qtys qtrm ctxt =
+fun derive_rtrm ctxt qtys qtrm =
subst_trm ctxt (mk_ty_subst qtys true ctxt) (mk_trm_subst qtys true ctxt) qtrm