1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 27 13:21:12 2011 +0200
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Wed Apr 27 19:27:06 2011 +0200
     1.3 @@ -440,7 +440,9 @@
     1.4        | tm_of (tab, _) (Ident s) =
     1.5            (case Symtab.lookup tab s of
     1.6               SOME t_ty => t_ty
     1.7 -           | NONE => error ("Undeclared identifier " ^ s))
     1.8 +           | NONE => (case lookup_prfx prfx pfuns s of
     1.9 +               SOME (SOME ([], resty), t) => (t, resty)
    1.10 +             | _ => error ("Undeclared identifier " ^ s)))
    1.11  
    1.12        | tm_of _ (Number i) = (HOLogic.mk_number HOLogic.intT i, integerN)
    1.13  
    1.14 @@ -696,8 +698,9 @@
    1.15            (fold_expr f g) (fold_opt (fold_expr f g)))))
    1.16          (fold_expr f g)) assocs;
    1.17  
    1.18 -val add_expr_pfuns = fold_expr
    1.19 -  (fn s => if is_pfun s then I else insert (op =) s) (K I);
    1.20 +fun add_expr_pfuns funs = fold_expr
    1.21 +  (fn s => if is_pfun s then I else insert (op =) s)
    1.22 +  (fn s => if is_none (lookup funs s) then I else insert (op =) s);
    1.23  
    1.24  val add_expr_idents = fold_expr (K I) (insert (op =));
    1.25  
    1.26 @@ -765,14 +768,14 @@
    1.27  fun fold_vcs f vcs =
    1.28    VCtab.fold (fn (_, (_, _, ps, cs)) => fold f ps #> fold f cs) vcs;
    1.29  
    1.30 -fun pfuns_of_vcs prfx pfuns vcs =
    1.31 -  fold_vcs (add_expr_pfuns o snd) vcs [] |>
    1.32 +fun pfuns_of_vcs prfx funs pfuns vcs =
    1.33 +  fold_vcs (add_expr_pfuns funs o snd) vcs [] |>
    1.34    filter (is_none o lookup_prfx prfx pfuns);
    1.35  
    1.36  fun declare_missing_pfuns thy prfx funs pfuns vcs (tab, ctxt) =
    1.37    let
    1.38      val (fs, (tys, Ts)) =
    1.39 -      pfuns_of_vcs prfx pfuns vcs |>
    1.40 +      pfuns_of_vcs prfx funs pfuns vcs |>
    1.41        map_filter (fn s => lookup funs s |>
    1.42          Option.map (fn ty => (s, (SOME ty, pfun_type thy prfx ty)))) |>
    1.43        split_list ||> split_list;
    1.44 @@ -963,15 +966,16 @@
    1.45    (map (fn ((s, i), _) => s ^ "(" ^ string_of_int i ^ ")") rules);
    1.46  
    1.47  (* sort definitions according to their dependency *)
    1.48 -fun sort_defs _ _ _ [] sdefs = rev sdefs
    1.49 -  | sort_defs prfx pfuns consts defs sdefs =
    1.50 +fun sort_defs _ _ _ _ [] sdefs = rev sdefs
    1.51 +  | sort_defs prfx funs pfuns consts defs sdefs =
    1.52        (case find_first (fn (_, (_, e)) =>
    1.53 -         forall (is_some o lookup_prfx prfx pfuns) (add_expr_pfuns e []) andalso
    1.54 +         forall (is_some o lookup_prfx prfx pfuns)
    1.55 +           (add_expr_pfuns funs e []) andalso
    1.56           forall (fn id =>
    1.57             member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
    1.58             consts id)
    1.59               (add_expr_idents e [])) defs of
    1.60 -         SOME d => sort_defs prfx pfuns consts
    1.61 +         SOME d => sort_defs prfx funs pfuns consts
    1.62             (remove (op =) d defs) (d :: sdefs)
    1.63         | NONE => error ("Bad definitions: " ^ rulenames defs));
    1.64  
    1.65 @@ -993,7 +997,7 @@
    1.66          (filter_out (is_trivial_vc o snd) vcs)) vcs);
    1.67  
    1.68      val _ = (case filter_out (is_some o lookup funs)
    1.69 -        (pfuns_of_vcs prfx pfuns vcs') of
    1.70 +        (pfuns_of_vcs prfx funs pfuns vcs') of
    1.71          [] => ()
    1.72        | fs => error ("Undeclared proof function(s) " ^ commas fs));
    1.73  
    1.74 @@ -1007,7 +1011,7 @@
    1.75        fold (snd oo add_const prfx) consts' |> (fn ids_thy as ((tab, _), _) =>
    1.76          ids_thy |>
    1.77          fold_map (add_def prfx types pfuns consts)
    1.78 -          (sort_defs prfx pfuns (Symtab.defined tab) defs []) ||>>
    1.79 +          (sort_defs prfx funs pfuns (Symtab.defined tab) defs []) ||>>
    1.80          fold_map (add_var prfx) (items vars) ||>>
    1.81          add_init_vars prfx vcs');
    1.82