1.1 --- a/src/Pure/thm.ML Wed Sep 30 19:04:48 2009 +0200
1.2 +++ b/src/Pure/thm.ML Wed Sep 30 22:20:58 2009 +0200
1.3 @@ -181,7 +181,7 @@
1.4 val sorts = Sorts.insert_typ T [];
1.5 in Ctyp {thy_ref = Theory.check_thy thy, T = T, maxidx = maxidx, sorts = sorts} end;
1.6
1.7 -fun dest_ctyp (Ctyp {thy_ref, T = Type (s, Ts), maxidx, sorts}) =
1.8 +fun dest_ctyp (Ctyp {thy_ref, T = Type (_, Ts), maxidx, sorts}) =
1.9 map (fn T => Ctyp {thy_ref = thy_ref, T = T, maxidx = maxidx, sorts = sorts}) Ts
1.10 | dest_ctyp cT = raise TYPE ("dest_ctyp", [typ_of cT], []);
1.11
1.12 @@ -218,31 +218,31 @@
1.13 val sorts = Sorts.insert_term t [];
1.14 in Cterm {thy_ref = Theory.check_thy thy, t = t, T = T, maxidx = maxidx, sorts = sorts} end;
1.15
1.16 -fun merge_thys0 (Cterm {thy_ref = r1, t = t1, ...}) (Cterm {thy_ref = r2, t = t2, ...}) =
1.17 +fun merge_thys0 (Cterm {thy_ref = r1, ...}) (Cterm {thy_ref = r2, ...}) =
1.18 Theory.merge_refs (r1, r2);
1.19
1.20
1.21 (* destructors *)
1.22
1.23 -fun dest_comb (ct as Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
1.24 +fun dest_comb (Cterm {t = c $ a, T, thy_ref, maxidx, sorts}) =
1.25 let val A = Term.argument_type_of c 0 in
1.26 (Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
1.27 Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
1.28 end
1.29 | dest_comb ct = raise CTERM ("dest_comb", [ct]);
1.30
1.31 -fun dest_fun (ct as Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
1.32 +fun dest_fun (Cterm {t = c $ _, T, thy_ref, maxidx, sorts}) =
1.33 let val A = Term.argument_type_of c 0
1.34 in Cterm {t = c, T = A --> T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
1.35 | dest_fun ct = raise CTERM ("dest_fun", [ct]);
1.36
1.37 -fun dest_arg (ct as Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
1.38 +fun dest_arg (Cterm {t = c $ a, T = _, thy_ref, maxidx, sorts}) =
1.39 let val A = Term.argument_type_of c 0
1.40 in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
1.41 | dest_arg ct = raise CTERM ("dest_arg", [ct]);
1.42
1.43
1.44 -fun dest_fun2 (Cterm {t = c $ a $ b, T, thy_ref, maxidx, sorts}) =
1.45 +fun dest_fun2 (Cterm {t = c $ _ $ _, T, thy_ref, maxidx, sorts}) =
1.46 let
1.47 val A = Term.argument_type_of c 0;
1.48 val B = Term.argument_type_of c 1;
1.49 @@ -254,8 +254,7 @@
1.50 in Cterm {t = a, T = A, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts} end
1.51 | dest_arg1 ct = raise CTERM ("dest_arg1", [ct]);
1.52
1.53 -fun dest_abs a (ct as
1.54 - Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
1.55 +fun dest_abs a (Cterm {t = Abs (x, T, t), T = Type ("fun", [_, U]), thy_ref, maxidx, sorts}) =
1.56 let val (y', t') = Term.dest_abs (the_default x a, T, t) in
1.57 (Cterm {t = Free (y', T), T = T, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts},
1.58 Cterm {t = t', T = U, thy_ref = thy_ref, maxidx = maxidx, sorts = sorts})
1.59 @@ -392,10 +391,10 @@
1.60
1.61 (* merge theories of cterms/thms -- trivial absorption only *)
1.62
1.63 -fun merge_thys1 (Cterm {thy_ref = r1, ...}) (th as Thm (_, {thy_ref = r2, ...})) =
1.64 +fun merge_thys1 (Cterm {thy_ref = r1, ...}) (Thm (_, {thy_ref = r2, ...})) =
1.65 Theory.merge_refs (r1, r2);
1.66
1.67 -fun merge_thys2 (th1 as Thm (_, {thy_ref = r1, ...})) (th2 as Thm (_, {thy_ref = r2, ...})) =
1.68 +fun merge_thys2 (Thm (_, {thy_ref = r1, ...})) (Thm (_, {thy_ref = r2, ...})) =
1.69 Theory.merge_refs (r1, r2);
1.70
1.71
1.72 @@ -808,7 +807,7 @@
1.73 (*Reflexivity
1.74 t == t
1.75 *)
1.76 -fun reflexive (ct as Cterm {thy_ref, t, T, maxidx, sorts}) =
1.77 +fun reflexive (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.78 Thm (deriv_rule0 Pt.reflexive,
1.79 {thy_ref = thy_ref,
1.80 tags = [],
1.81 @@ -825,7 +824,7 @@
1.82 *)
1.83 fun symmetric (th as Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
1.84 (case prop of
1.85 - (eq as Const ("==", Type (_, [T, _]))) $ t $ u =>
1.86 + (eq as Const ("==", _)) $ t $ u =>
1.87 Thm (deriv_rule1 Pt.symmetric der,
1.88 {thy_ref = thy_ref,
1.89 tags = [],
1.90 @@ -868,7 +867,7 @@
1.91 (%x. t)(u) == t[u/x]
1.92 fully beta-reduces the term if full = true
1.93 *)
1.94 -fun beta_conversion full (Cterm {thy_ref, t, T, maxidx, sorts}) =
1.95 +fun beta_conversion full (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.96 let val t' =
1.97 if full then Envir.beta_norm t
1.98 else
1.99 @@ -885,7 +884,7 @@
1.100 prop = Logic.mk_equals (t, t')})
1.101 end;
1.102
1.103 -fun eta_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
1.104 +fun eta_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.105 Thm (deriv_rule0 Pt.reflexive,
1.106 {thy_ref = thy_ref,
1.107 tags = [],
1.108 @@ -895,7 +894,7 @@
1.109 tpairs = [],
1.110 prop = Logic.mk_equals (t, Envir.eta_contract t)});
1.111
1.112 -fun eta_long_conversion (Cterm {thy_ref, t, T, maxidx, sorts}) =
1.113 +fun eta_long_conversion (Cterm {thy_ref, t, T = _, maxidx, sorts}) =
1.114 Thm (deriv_rule0 Pt.reflexive,
1.115 {thy_ref = thy_ref,
1.116 tags = [],
1.117 @@ -951,7 +950,7 @@
1.118 prop = prop2, ...}) = th2;
1.119 fun chktypes fT tT =
1.120 (case fT of
1.121 - Type ("fun", [T1, T2]) =>
1.122 + Type ("fun", [T1, _]) =>
1.123 if T1 <> tT then
1.124 raise THM ("combination: types", 0, [th1, th2])
1.125 else ()
1.126 @@ -1264,7 +1263,7 @@
1.127 val varifyT = #2 o varifyT' [];
1.128
1.129 (* Replace all TVars by new TFrees *)
1.130 -fun freezeT (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) =
1.131 +fun freezeT (Thm (der, {thy_ref, shyps, hyps, tpairs, prop, ...})) =
1.132 let
1.133 val prop1 = attach_tpairs tpairs prop;
1.134 val prop2 = Type.freeze prop1;
1.135 @@ -1329,7 +1328,7 @@
1.136 (*Solve subgoal Bi of proof state B1...Bn/C by assumption. *)
1.137 fun assumption i state =
1.138 let
1.139 - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
1.140 + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
1.141 val thy = Theory.deref thy_ref;
1.142 val (tpairs, Bs, Bi, C) = dest_state (state, i);
1.143 fun newth n (env, tpairs) =
1.144 @@ -1365,7 +1364,7 @@
1.145 Checks if Bi's conclusion is alpha-convertible to one of its assumptions*)
1.146 fun eq_assumption i state =
1.147 let
1.148 - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
1.149 + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
1.150 val (tpairs, Bs, Bi, C) = dest_state (state, i);
1.151 val (_, asms, concl) = Logic.assum_problems (~1, Bi);
1.152 in
1.153 @@ -1386,7 +1385,7 @@
1.154 (*For rotate_tac: fast rotation of assumptions of subgoal i*)
1.155 fun rotate_rule k i state =
1.156 let
1.157 - val Thm (der, {thy_ref, maxidx, shyps, hyps, prop, ...}) = state;
1.158 + val Thm (der, {thy_ref, maxidx, shyps, hyps, ...}) = state;
1.159 val (tpairs, Bs, Bi, C) = dest_state (state, i);
1.160 val params = Term.strip_all_vars Bi
1.161 and rest = Term.strip_all_body Bi;
1.162 @@ -1558,7 +1557,7 @@
1.163 in Term.all T' $ Abs (a, T', norm_term_skip env n t) end
1.164 | norm_term_skip env n (Const ("==>", _) $ A $ B) =
1.165 Logic.mk_implies (A, norm_term_skip env (n - 1) B)
1.166 - | norm_term_skip env n t = error "norm_term_skip: too few assumptions??";
1.167 + | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??";
1.168
1.169
1.170 (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C)