src/Pure/Isar/code_unit.ML
changeset 28708 a1a436f09ec6
parent 28704 8703d17c5e68
child 29270 0eade173f77e
     1.1 --- a/src/Pure/Isar/code_unit.ML	Tue Oct 28 17:53:46 2008 +0100
     1.2 +++ b/src/Pure/Isar/code_unit.ML	Wed Oct 29 11:33:40 2008 +0100
     1.3 @@ -38,7 +38,7 @@
     1.4    (*defining equations*)
     1.5    val assert_eqn: theory -> thm -> thm
     1.6    val mk_eqn: theory -> thm -> thm * bool
     1.7 -  val assert_linear: thm * bool -> thm * bool
     1.8 +  val assert_linear: (string -> bool) -> thm * bool -> thm * bool
     1.9    val const_eqn: thm -> string
    1.10    val const_typ_eqn: thm -> string * typ
    1.11    val head_eqn: theory -> thm -> string * ((string * sort) list * typ)
    1.12 @@ -377,8 +377,17 @@
    1.13        ((fold o fold_aterms) (fn Var (v, _) => cons v | _ => I) args []))
    1.14    in (thm, linear) end;
    1.15  
    1.16 -fun assert_linear (thm, false) = (thm, false)
    1.17 -  | assert_linear (thm, true) = if snd (add_linear thm) then (thm, true)
    1.18 +fun assert_pat is_cons thm =
    1.19 +  let
    1.20 +    val args = (snd o strip_comb o fst o Logic.dest_equals o Thm.plain_prop_of) thm;
    1.21 +    val _ = (map o map_aterms) (fn t as Const (c, _) => if is_cons c then t
    1.22 +          else bad_thm ("Not a constructor on left hand side of equation: "
    1.23 +            ^ quote c ^ ",\n in equation\n" ^ Display.string_of_thm thm)
    1.24 +      | t => t) args;
    1.25 +  in thm end;
    1.26 +
    1.27 +fun assert_linear is_cons (thm, false) = (thm, false)
    1.28 +  | assert_linear is_cons (thm, true) = if snd (add_linear (assert_pat is_cons thm)) then (thm, true)
    1.29        else bad_thm
    1.30          ("Duplicate variables on left hand side of defining equation:\n"
    1.31            ^ Display.string_of_thm thm);