more explicit error on malformed abstract equation; dropped dead code; tuned signature
authorhaftmann
Sat Feb 18 11:31:35 2012 +0100 (2012-02-18)
changeset 465132659ee0128c2
parent 46512 4f9f61f9b535
child 46514 4f7780086991
more explicit error on malformed abstract equation; dropped dead code; tuned signature
src/Pure/Isar/code.ML
     1.1 --- a/src/Pure/Isar/code.ML	Fri Feb 17 15:42:26 2012 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Sat Feb 18 11:31:35 2012 +0100
     1.3 @@ -49,6 +49,7 @@
     1.4        -> theory -> theory) -> theory -> theory
     1.5    val add_eqn: thm -> theory -> theory
     1.6    val add_nbe_eqn: thm -> theory -> theory
     1.7 +  val add_abs_eqn: thm -> theory -> theory
     1.8    val add_default_eqn: thm -> theory -> theory
     1.9    val add_default_eqn_attribute: attribute
    1.10    val add_default_eqn_attrib: Attrib.src
    1.11 @@ -114,8 +115,6 @@
    1.12  
    1.13  (* constants *)
    1.14  
    1.15 -fun typ_equiv tys = Type.raw_instance tys andalso Type.raw_instance (swap tys);
    1.16 -
    1.17  fun check_bare_const thy t = case try dest_Const t
    1.18   of SOME c_ty => c_ty
    1.19    | NONE => error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
    1.20 @@ -517,7 +516,8 @@
    1.21             | THM _ => bad "Not a proper equation";
    1.22      val (rep, lhs) = dest_comb full_lhs
    1.23        handle TERM _ => bad "Not an abstract equation";
    1.24 -    val (rep_const, ty) = dest_Const rep;
    1.25 +    val (rep_const, ty) = dest_Const rep
    1.26 +      handle TERM _ => bad "Not an abstract equation";
    1.27      val (tyco, Ts) = (dest_Type o domain_type) ty
    1.28        handle TERM _ => bad "Not an abstract equation"
    1.29             | TYPE _ => bad "Not an abstract equation";
    1.30 @@ -697,8 +697,7 @@
    1.31      val add_consts = fold_aterms add_const
    1.32    in add_consts rhs o fold add_consts args end;
    1.33  
    1.34 -fun dest_eqn thy =
    1.35 -  apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
    1.36 +val dest_eqn = apfst (snd o strip_comb) o Logic.dest_equals o Logic.unvarify_global;
    1.37  
    1.38  abstype cert = Equations of thm * bool list
    1.39    | Projection of term * string
    1.40 @@ -809,21 +808,21 @@
    1.41            |> Thm.varifyT_global
    1.42            |> Conjunction.elim_balanced (length propers);
    1.43          fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, NONE));
    1.44 -      in (tyscm, map (abstractions o dest_eqn thy o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
    1.45 +      in (tyscm, map (abstractions o dest_eqn o Thm.prop_of) thms ~~ (map SOME thms ~~ propers)) end
    1.46    | equations_of_cert thy (Projection (t, tyco)) =
    1.47        let
    1.48          val (_, ((abs, _), _)) = get_abstype_spec thy tyco;
    1.49          val tyscm = typscheme_projection thy t;
    1.50          val t' = Logic.varify_types_global t;
    1.51          fun abstractions (args, rhs) = (map (rpair (SOME abs)) args, (rhs, NONE));
    1.52 -      in (tyscm, [((abstractions o dest_eqn thy) t', (NONE, true))]) end
    1.53 +      in (tyscm, [((abstractions o dest_eqn) t', (NONE, true))]) end
    1.54    | equations_of_cert thy (Abstract (abs_thm, tyco)) =
    1.55        let
    1.56          val tyscm = typscheme_abs thy abs_thm;
    1.57          val (abs, concrete_thm) = concretify_abs thy tyco abs_thm;
    1.58          fun abstractions (args, rhs) = (map (rpair NONE) args, (rhs, (SOME abs)));
    1.59        in
    1.60 -        (tyscm, [((abstractions o dest_eqn thy o Thm.prop_of) concrete_thm,
    1.61 +        (tyscm, [((abstractions o dest_eqn o Thm.prop_of) concrete_thm,
    1.62            (SOME (Thm.varifyT_global abs_thm), true))])
    1.63        end;
    1.64