1.1 --- a/src/HOL/Tools/function_package/fundef_common.ML	Fri Jun 01 15:20:53 2007 +0200
     1.2 +++ b/src/HOL/Tools/function_package/fundef_common.ML	Fri Jun 01 15:57:45 2007 +0200
     1.3 @@ -224,6 +224,51 @@
     1.4    fun fundef_parser default_cfg = config_parser default_cfg -- P.fixes --| P.$$$ "where" -- statements_ow
     1.5  end
     1.6  
     1.7 +
     1.8 +
     1.9 +(* Common operations on equations *)
    1.10 +
    1.11 +fun open_all_all (Const ("all", _) $ Abs (n, T, b)) = apfst (cons (n, T)) (open_all_all b)
    1.12 +  | open_all_all t = ([], t)
    1.13 +
    1.14 +exception MalformedEquation of term
    1.15 +
    1.16 +fun split_def geq =
    1.17 +    let
    1.18 +      val (qs, imp) = open_all_all geq
    1.19 +
    1.20 +      val gs = Logic.strip_imp_prems imp
    1.21 +      val eq = Logic.strip_imp_concl imp
    1.22 +
    1.23 +      val (f_args, rhs) = HOLogic.dest_eq (HOLogic.dest_Trueprop eq)
    1.24 +          handle TERM _ => raise MalformedEquation geq
    1.25 +
    1.26 +      val (head, args) = strip_comb f_args
    1.27 +
    1.28 +      val fname = fst (dest_Free head)
    1.29 +          handle TERM _ => raise MalformedEquation geq
    1.30 +    in
    1.31 +      (fname, qs, gs, args, rhs)
    1.32 +    end
    1.33 +
    1.34 +exception ArgumentCount of string
    1.35 +
    1.36 +fun mk_arities fqgars =
    1.37 +    let fun f (fname, _, _, args, _) arities =
    1.38 +            let val k = length args
    1.39 +            in
    1.40 +              case Symtab.lookup arities fname of
    1.41 +                NONE => Symtab.update (fname, k) arities
    1.42 +              | SOME i => (if i = k then arities else raise ArgumentCount fname)
    1.43 +            end
    1.44 +    in
    1.45 +      fold f fqgars Symtab.empty
    1.46 +    end
    1.47 +
    1.48 +
    1.49 +
    1.50 +
    1.51 +
    1.52  end
    1.53  
    1.54  (* Common Abbreviations *)