src/Pure/Isar/code.ML
changeset 28708 a1a436f09ec6
parent 28703 aef727ef30e5
child 28971 300ec36a19af
     1.1 --- a/src/Pure/Isar/code.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -462,13 +462,6 @@
     1.4            cons (Thm.ctyp_of thy (TVar (x_i, sort)), Thm.ctyp_of thy ty)) env [];
     1.5        in map (Thm.instantiate (instT, [])) thms' end;
     1.6  
     1.7 -fun certify_const thy c eqns =
     1.8 -  let
     1.9 -    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
    1.10 -      then eqn else error ("Wrong head of defining equation,\nexpected constant "
    1.11 -        ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    1.12 -  in map cert eqns end;
    1.13 -
    1.14  fun check_linear (eqn as (thm, linear)) =
    1.15    if linear then eqn else Code_Unit.bad_thm
    1.16      ("Duplicate variables on left hand side of defining equation:\n"
    1.17 @@ -542,6 +535,16 @@
    1.18          in SOME (Logic.varifyT ty) end
    1.19      | NONE => NONE;
    1.20  
    1.21 +fun recheck_eqn thy = Code_Unit.error_thm
    1.22 +  (Code_Unit.assert_linear (is_some o get_datatype_of_constr thy) o apfst (Code_Unit.assert_eqn thy));
    1.23 +
    1.24 +fun recheck_eqns_const thy c eqns =
    1.25 +  let
    1.26 +    fun cert (eqn as (thm, _)) = if c = Code_Unit.const_eqn thm
    1.27 +      then eqn else error ("Wrong head of defining equation,\nexpected constant "
    1.28 +        ^ Code_Unit.string_of_const thy c ^ "\n" ^ Display.string_of_thm thm)
    1.29 +  in map (cert o recheck_eqn thy) eqns end;
    1.30 +
    1.31  fun change_eqns delete c f = (map_exec_purge (SOME [c]) o map_eqns
    1.32    o (if delete then Symtab.map_entry c else Symtab.map_default (c, ((false, (true, Lazy.value [])), [])))
    1.33      o apfst) (fn (_, eqns) => (true, f eqns));
    1.34 @@ -568,8 +571,7 @@
    1.35  
    1.36  fun add_eqnl (c, lthms) thy =
    1.37    let
    1.38 -    val lthms' = certificate thy
    1.39 -      (fn thy => map (Code_Unit.assert_linear) o certify_const thy c) lthms;
    1.40 +    val lthms' = certificate thy (fn thy => recheck_eqns_const thy c) lthms;
    1.41    in change_eqns false c (add_lthms lthms') thy end;
    1.42  
    1.43  val add_default_eqn_attribute = Thm.declaration_attribute
    1.44 @@ -660,8 +662,7 @@
    1.45    | apply_functrans thy c functrans eqns = eqns
    1.46        |> perhaps (perhaps_loop (perhaps_apply functrans))
    1.47        |> (map o apfst) (AxClass.unoverload thy)
    1.48 -      |> (map o Code_Unit.error_thm) (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
    1.49 -      |> certify_const thy c
    1.50 +      |> recheck_eqns_const thy c
    1.51        |> (map o apfst) (AxClass.overload thy);
    1.52  
    1.53  fun rhs_conv conv thm = Thm.transitive thm ((conv o Thm.rhs_of) thm);
    1.54 @@ -682,7 +683,7 @@
    1.55      |> apply_functrans thy c functrans
    1.56      |> (map o apfst) (Code_Unit.rewrite_eqn pre)
    1.57      |> (map o apfst) (AxClass.unoverload thy)
    1.58 -    |> map (Code_Unit.assert_linear o apfst (Code_Unit.assert_eqn thy))
    1.59 +    |> map (recheck_eqn thy)
    1.60      |> burrow_fst (common_typ_eqns thy)
    1.61    end;
    1.62