1.1 --- a/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Mar 03 15:59:44 2011 +1100
     1.2 +++ b/src/HOL/SPARK/Tools/spark_vcs.ML	Thu Mar 03 11:01:42 2011 +0100
     1.3 @@ -768,14 +768,16 @@
     1.4       SOME ty =>
     1.5         let
     1.6           val (t, ty') = term_of_expr thy types funs pfuns ids e;
     1.7 -         val _ = ty = ty' orelse
     1.8 +         val T = mk_type thy ty;
     1.9 +         val T' = mk_type thy ty';
    1.10 +         val _ = T = T' orelse
    1.11             error ("Declared type " ^ ty ^ " of " ^ s ^
    1.12               "\ndoes not match type " ^ ty' ^ " in definition");
    1.13           val id' = mk_rulename id;
    1.14           val lthy = Named_Target.theory_init thy;
    1.15           val ((t', (_, th)), lthy') = Specification.definition
    1.16             (NONE, ((id', []), HOLogic.mk_Trueprop (HOLogic.mk_eq
    1.17 -             (Free (s, mk_type thy ty), t)))) lthy;
    1.18 +             (Free (s, T), t)))) lthy;
    1.19           val phi = ProofContext.export_morphism lthy' lthy
    1.20         in
    1.21           ((id', Morphism.thm phi th),
    1.22 @@ -813,7 +815,7 @@
    1.23           forall (Symtab.defined pfuns) (add_expr_pfuns e []) andalso
    1.24           forall (fn id =>
    1.25             member (fn (s, (_, (s', _))) => s = s') sdefs id orelse
    1.26 -           member (fn (s, (s', _)) => s = s') consts id)
    1.27 +           consts id)
    1.28               (add_expr_idents e [])) defs of
    1.29           SOME d => sort_defs pfuns consts
    1.30             (remove (op =) d defs) (d :: sdefs)
    1.31 @@ -822,10 +824,9 @@
    1.32  fun set_vcs ({types, vars, consts, funs} : decls) (rules, _) vcs path thy =
    1.33    let
    1.34      val {pfuns, ...} = VCs.get thy;
    1.35 -    val (defs', rules') = partition_opt dest_def rules;
    1.36 +    val (defs, rules') = partition_opt dest_def rules;
    1.37      val consts' =
    1.38 -      subtract (fn ((_, (s, _)), (s', _)) => s = s') defs' (items consts);
    1.39 -    val defs = sort_defs pfuns consts' defs' [];
    1.40 +      subtract (fn ((_, (s, _)), (s', _)) => s = s') defs (items consts);
    1.41      (* ignore all complex rules in rls files *)
    1.42      val (rules'', other_rules) =
    1.43        List.partition (complex_rule o snd) rules';
    1.44 @@ -847,10 +848,12 @@
    1.45          Symtab.update ("true", (HOLogic.true_const, booleanN)),
    1.46          Name.context), thy) |>
    1.47        fold add_type_def (items types) |>
    1.48 -      fold (snd oo add_const) consts' |>
    1.49 -      fold_map (add_def types funs pfuns consts) defs ||>>
    1.50 -      fold_map add_var (items vars) ||>>
    1.51 -      add_init_vars vcs';
    1.52 +      fold (snd oo add_const) consts' |> (fn ids_thy as ((tab, _), _) =>
    1.53 +        ids_thy |>
    1.54 +        fold_map (add_def types funs pfuns consts)
    1.55 +          (sort_defs pfuns (Symtab.defined tab) defs []) ||>>
    1.56 +        fold_map add_var (items vars) ||>>
    1.57 +        add_init_vars vcs');
    1.58  
    1.59      val ctxt =
    1.60        [Element.Fixes (map (fn (s, T) =>