renamed const_deps to defs;
authorwenzelm
Sun Jun 05 23:07:29 2005 +0200 (2005-06-05)
changeset 16291ea4e64b2f25a
parent 16290 e661e37a4d50
child 16292 fbe2fc30a177
renamed const_deps to defs;
improved error messages;
major cleanup -- removed quite a bit of dead code;
src/Pure/theory.ML
     1.1 --- a/src/Pure/theory.ML	Sun Jun 05 23:07:28 2005 +0200
     1.2 +++ b/src/Pure/theory.ML	Sun Jun 05 23:07:29 2005 +0200
     1.3 @@ -4,13 +4,14 @@
     1.4  
     1.5  The abstract type "theory" of theories.
     1.6  *)
     1.7 +
     1.8  signature BASIC_THEORY =
     1.9  sig
    1.10    type theory
    1.11    exception THEORY of string * theory list
    1.12    val rep_theory: theory ->
    1.13      {sign: Sign.sg,
    1.14 -      const_deps: Defs.graph,
    1.15 +      defs: Defs.graph,
    1.16        axioms: term Symtab.table,
    1.17        oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    1.18        parents: theory list,
    1.19 @@ -118,7 +119,6 @@
    1.20    val put_data: Object.kind -> ('a -> Object.T) -> 'a -> theory -> theory
    1.21  end;
    1.22  
    1.23 -
    1.24  structure Theory: PRIVATE_THEORY =
    1.25  struct
    1.26  
    1.27 @@ -128,14 +128,14 @@
    1.28  datatype theory =
    1.29    Theory of {
    1.30      sign: Sign.sg,
    1.31 -    const_deps: Defs.graph,
    1.32 +    defs: Defs.graph,
    1.33      axioms: term Symtab.table,
    1.34      oracles: ((Sign.sg * Object.T -> term) * stamp) Symtab.table,
    1.35      parents: theory list,
    1.36      ancestors: theory list};
    1.37  
    1.38 -fun make_theory sign const_deps axioms oracles parents ancestors =
    1.39 -  Theory {sign = sign, const_deps = const_deps, axioms = axioms,
    1.40 +fun make_theory sign defs axioms oracles parents ancestors =
    1.41 +  Theory {sign = sign, defs = defs, axioms = axioms,
    1.42      oracles = oracles, parents = parents, ancestors = ancestors};
    1.43  
    1.44  fun rep_theory (Theory args) = args;
    1.45 @@ -185,19 +185,15 @@
    1.46  
    1.47  fun ext_theory thy ext_sg new_axms new_oras =
    1.48    let
    1.49 -    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy
    1.50 -    val draft = Sign.is_draft sign
    1.51 -    val axioms' =
    1.52 -      Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
    1.53 -        handle Symtab.DUPS names => err_dup_axms names
    1.54 -    val oracles' =
    1.55 -      Symtab.extend (oracles, new_oras)
    1.56 -        handle Symtab.DUPS names => err_dup_oras names
    1.57 +    val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
    1.58 +    val draft = Sign.is_draft sign;
    1.59 +    val axioms' = Symtab.extend (if draft then axioms else Symtab.empty, new_axms)
    1.60 +      handle Symtab.DUPS names => err_dup_axms names;
    1.61 +    val oracles' = Symtab.extend (oracles, new_oras)
    1.62 +      handle Symtab.DUPS names => err_dup_oras names;
    1.63      val (parents', ancestors') =
    1.64 -      if draft then (parents, ancestors) else ([thy], thy :: ancestors)
    1.65 -  in
    1.66 -    make_theory (ext_sg sign) const_deps axioms' oracles' parents' ancestors'
    1.67 -  end;
    1.68 +      if draft then (parents, ancestors) else ([thy], thy :: ancestors);
    1.69 +  in make_theory (ext_sg sign) defs axioms' oracles' parents' ancestors' end;
    1.70  
    1.71  
    1.72  (* extend signature of a theory *)
    1.73 @@ -260,22 +256,23 @@
    1.74  fun err_in_axm name =
    1.75    error ("The error(s) above occurred in axiom " ^ quote name);
    1.76  
    1.77 -fun no_vars sg tm = (case (term_vars tm, term_tvars tm) of
    1.78 +fun no_vars pp tm =
    1.79 +  (case (Term.term_vars tm, Term.term_tvars tm) of
    1.80      ([], []) => tm
    1.81    | (ts, ixns) => error (Pretty.string_of (Pretty.block (Pretty.breaks
    1.82        (Pretty.str "Illegal schematic variable(s) in term:" ::
    1.83 -       map (Sign.pretty_term sg) ts @
    1.84 -       map (Sign.pretty_typ sg o TVar) ixns)))));
    1.85 +       map (Pretty.term pp) ts @ map (Pretty.typ pp o TVar) ixns)))));
    1.86  
    1.87  fun cert_axm sg (name, raw_tm) =
    1.88    let
    1.89 -    val (t, T, _) = Sign.certify_term (Sign.pp sg) sg raw_tm
    1.90 +    val pp = Sign.pp sg;
    1.91 +    val (t, T, _) = Sign.certify_term pp sg raw_tm
    1.92        handle TYPE (msg, _, _) => error msg
    1.93 -           | TERM (msg, _) => error msg;
    1.94 +        | TERM (msg, _) => error msg;
    1.95    in
    1.96      Term.no_dummy_patterns t handle TERM (msg, _) => error msg;
    1.97      assert (T = propT) "Term not of type prop";
    1.98 -    (name, no_vars sg t)
    1.99 +    (name, no_vars pp t)
   1.100    end;
   1.101  
   1.102  (*some duplication of code with read_def_cterm*)
   1.103 @@ -289,24 +286,32 @@
   1.104  fun read_axm sg name_str = read_def_axm (sg, K NONE, K NONE) [] name_str;
   1.105  
   1.106  fun inferT_axm sg (name, pre_tm) =
   1.107 -  let val (t, _) = Sign.infer_types (Sign.pp sg) sg
   1.108 -    (K NONE) (K NONE) [] true ([pre_tm], propT);
   1.109 -  in (name, no_vars sg t) end
   1.110 +  let
   1.111 +    val pp = Sign.pp sg;
   1.112 +    val (t, _) = Sign.infer_types pp sg (K NONE) (K NONE) [] true ([pre_tm], propT);
   1.113 +  in (name, no_vars pp t) end
   1.114    handle ERROR => err_in_axm name;
   1.115  
   1.116  
   1.117  (* extend axioms of a theory *)
   1.118  
   1.119 -fun ext_axms prep_axm raw_axms (thy as Theory {sign, ...}) =
   1.120 +local
   1.121 +
   1.122 +fun gen_add_axioms prep_axm raw_axms thy =
   1.123    let
   1.124 -    val raw_axms' = map (apfst (Sign.full_name sign)) raw_axms;
   1.125 +    val sg = sign_of thy;
   1.126 +    val raw_axms' = map (apfst (Sign.full_name sg)) raw_axms;
   1.127      val axioms =
   1.128 -      map (apsnd (Term.compress_term o Logic.varify) o prep_axm sign) raw_axms';
   1.129 +      map (apsnd (Term.compress_term o Logic.varify) o prep_axm sg) raw_axms';
   1.130      val ext_sg = Sign.add_space (axiomK, map fst axioms);
   1.131    in ext_theory thy ext_sg axioms [] end;
   1.132  
   1.133 -val add_axioms = ext_axms read_axm;
   1.134 -val add_axioms_i = ext_axms cert_axm;
   1.135 +in
   1.136 +
   1.137 +val add_axioms = gen_add_axioms read_axm;
   1.138 +val add_axioms_i = gen_add_axioms cert_axm;
   1.139 +
   1.140 +end;
   1.141  
   1.142  
   1.143  (* add oracle **)
   1.144 @@ -323,195 +328,188 @@
   1.145  
   1.146  (* overloading *)
   1.147  
   1.148 -datatype overloading = NoOverloading | Useless | Plain;
   1.149 +datatype overloading = Clean | Implicit | Useless;
   1.150  
   1.151 -fun overloading sg declT defT =
   1.152 -  let val T = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT) in
   1.153 -    if Sign.typ_instance sg (declT, T) then NoOverloading
   1.154 -    else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts T) then Useless
   1.155 -    else Plain
   1.156 +fun overloading sg overloaded declT defT =
   1.157 +  let
   1.158 +    val defT' = Term.incr_tvar (maxidx_of_typ declT + 1) (Type.varifyT defT);
   1.159 +  in
   1.160 +    if Sign.typ_instance sg (declT, defT') then Clean
   1.161 +    else if Sign.typ_instance sg (Type.strip_sorts declT, Type.strip_sorts defT') then Useless
   1.162 +    else if overloaded then Clean
   1.163 +    else Implicit
   1.164    end;
   1.165  
   1.166 -(* dest_defn *)
   1.167  
   1.168 -fun dest_defn tm =
   1.169 +(* dest_def *)
   1.170 +
   1.171 +fun dest_def pp tm =
   1.172    let
   1.173      fun err msg = raise TERM (msg, [tm]);
   1.174  
   1.175      val (lhs, rhs) = Logic.dest_equals (Logic.strip_imp_concl tm)
   1.176        handle TERM _ => err "Not a meta-equality (==)";
   1.177 -    val (head, args) = strip_comb lhs;
   1.178 -    val c_ty as (c, ty) = dest_Const head
   1.179 +    val (head, args) = Term.strip_comb lhs;
   1.180 +    val (c, T) = Term.dest_Const head
   1.181        handle TERM _ => err "Head of lhs not a constant";
   1.182  
   1.183      fun dest_free (Free (x, _)) = x
   1.184        | dest_free (Const ("TYPE", Type ("itself", [TFree (x, _)]))) = x
   1.185        | dest_free _ = raise Match;
   1.186  
   1.187 +    val show_terms = commas_quote o map (Pretty.string_of_term pp);
   1.188      val show_frees = commas_quote o map dest_free;
   1.189      val show_tfrees = commas_quote o map fst;
   1.190  
   1.191 +    val lhs_nofrees = filter (not o can dest_free) args;
   1.192      val lhs_dups = duplicates args;
   1.193 -    val rhs_extras = gen_rems (op =) (term_frees rhs, args);
   1.194 -    val rhs_extrasT = gen_rems (op =) (term_tfrees rhs, typ_tfrees ty);
   1.195 +    val rhs_extras = term_frees rhs |> fold (remove op =) args;
   1.196 +    val rhs_extrasT = term_tfrees rhs |> fold (remove op =) (typ_tfrees T);
   1.197    in
   1.198 -    if not (forall (can dest_free) args) then
   1.199 -      err "Arguments (on lhs) must be variables"
   1.200 +    if not (null lhs_nofrees) then
   1.201 +      err ("Non-variables as arguments on lhs: " ^ show_terms lhs_nofrees)
   1.202      else if not (null lhs_dups) then
   1.203        err ("Duplicate variables on lhs: " ^ show_frees lhs_dups)
   1.204      else if not (null rhs_extras) then
   1.205        err ("Extra variables on rhs: " ^ show_frees rhs_extras)
   1.206      else if not (null rhs_extrasT) then
   1.207        err ("Extra type variables on rhs: " ^ show_tfrees rhs_extrasT)
   1.208 -    else if exists_Const (fn c_ty' => c_ty' = c_ty) rhs then
   1.209 +    else if exists_Const (equal (c, T)) rhs then
   1.210        err ("Constant to be defined occurs on rhs")
   1.211 -    else (c_ty, rhs)
   1.212 +    else ((c, T), rhs)
   1.213    end;
   1.214  
   1.215  
   1.216 -(* check_defn *)
   1.217 +(* check_def *)
   1.218 +
   1.219 +fun pretty_const pp (c, T) =
   1.220 + [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   1.221 +  Pretty.quote (Pretty.typ pp (Type.freeze_type T))];    (* FIXME zero indexes!? *)
   1.222  
   1.223 -fun err_in_defn sg name msg =
   1.224 -  error (cat_lines [msg, "The error(s) above occurred in definition " ^ quote name]);
   1.225 +(* FIXME move error messages to defs.ML !? *)
   1.226  
   1.227 -fun pretty_const sg (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   1.228 +fun pretty_path pp path = fold_rev (fn (T, c, def) =>
   1.229 +  fn [] => [Pretty.block (pretty_const pp (c, T))]
   1.230 +   | prts => Pretty.block (pretty_const pp (c, T) @
   1.231 +      [Pretty.brk 1, Pretty.str ("depends via " ^ quote def ^ " on")]) :: prts) path [];
   1.232  
   1.233 -fun cycle_msg sg (infinite, namess) = 
   1.234 -  let val header = if not (infinite) then "cyclic dependency found: " else "infinite chain found: "
   1.235 -  in
   1.236 -      Pretty.string_of (Pretty.block (((Pretty.str header) :: Pretty.fbrk :: (
   1.237 -        let      
   1.238 -	    fun f last (ty, constname, defname) =  
   1.239 -		(pretty_const sg (constname, ty)) @ (if last then [] else [Pretty.str (" depends via "^ quote defname^ " on ")])
   1.240 -          	
   1.241 -	in
   1.242 -	    foldr (fn (x,r) => (f (r=[]) x)@[Pretty.fbrk]@r) [] namess
   1.243 -	end))))
   1.244 -  end
   1.245 +fun defs_circular pp path =
   1.246 +  Pretty.str "Cyclic dependency in definitions: " :: pretty_path pp path
   1.247 +  |> Pretty.chunks |> Pretty.string_of;
   1.248 +
   1.249 +fun defs_infinite_chain pp path =
   1.250 +  Pretty.str "Infinite chain in definitions: " :: pretty_path pp path
   1.251 +  |> Pretty.chunks |> Pretty.string_of;
   1.252 +
   1.253 +fun defs_clash def1 def2 = "Type clash in definitions " ^ quote def1 ^ " and " ^ quote def2;
   1.254  
   1.255 -fun check_defn sg overloaded ((deps, axms), def as (bname, tm)) =
   1.256 -  let
   1.257 -    val name = Sign.full_name sg bname;
   1.258 -      
   1.259 -    fun pretty_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
   1.260 -      Pretty.quote (Sign.pretty_typ sg (#1 (Type.freeze_thaw_type ty)))];
   1.261 +fun defs_final pp const =
   1.262 +  (Pretty.str "Attempt to define final constant" :: Pretty.brk 1 :: pretty_const pp const)
   1.263 +  |> Pretty.block |> Pretty.string_of;
   1.264  
   1.265 -    fun def_txt (c_ty, txt) = Pretty.block
   1.266 -      (Pretty.str "Definition of " :: pretty_const c_ty @
   1.267 -        (if txt = "" then [] else [Pretty.str txt]));
   1.268 +(* FIXME move to defs.ML; avoid exceptions *)
   1.269 +fun declare sg c defs =
   1.270 +  let val T = Sign.the_const_type sg c
   1.271 +  in if_none (try (Defs.declare defs) (c, T)) defs end;
   1.272  
   1.273 -    fun show_defn c (dfn, ty') = Pretty.block
   1.274 -      (Pretty.str "  " :: pretty_const (c, ty') @ [Pretty.str " in ", Pretty.str dfn]);
   1.275 -
   1.276 -    val (c_ty as (c, ty), rhs) = dest_defn tm
   1.277 -      handle TERM (msg, _) => err_in_defn sg name msg;
   1.278  
   1.279 -    fun decl deps c = 
   1.280 -	(case Sign.const_type sg c of 
   1.281 -	     SOME T => (Defs.declare deps (c, T) handle _ => deps, T)
   1.282 -	   | NONE => err_in_defn sg name ("Undeclared constant " ^ quote c));
   1.283 +fun check_def sg overloaded (bname, tm) defs =
   1.284 +  let
   1.285 +    val pp = Sign.pp sg;
   1.286 +    val name = Sign.full_name sg bname;
   1.287 +
   1.288 +    fun err msg = error (Pretty.string_of (Pretty.chunks
   1.289 +     [Pretty.str msg,
   1.290 +      Pretty.block [Pretty.str ("The error(s) above occurred in definition " ^ quote name ^ ":"),
   1.291 +        Pretty.fbrk, Pretty.quote (Pretty.term pp tm)]]));
   1.292 +
   1.293 +    fun show_def const txt =
   1.294 +      [Pretty.block (Pretty.str "Definition of " :: pretty_const pp const), Pretty.str txt]
   1.295 +      |> Pretty.chunks |> Pretty.string_of;
   1.296  
   1.297 -    val (deps, c_decl) = decl deps c
   1.298 +    val ((c, defT), rhs) = dest_def pp tm handle TERM (msg, _) => err msg;
   1.299 +    val rhs_consts = Term.term_constsT rhs;
   1.300 +    val declT = Sign.the_const_type sg c;
   1.301  
   1.302 -    val body = Term.term_constsT rhs
   1.303 -    val deps = foldl (fn ((c, _), deps) => fst (decl deps c)) deps body
   1.304 +    val _ =
   1.305 +      (case overloading sg overloaded declT defT of
   1.306 +        Clean => ()
   1.307 +      | Implicit => warning (show_def (c, defT)
   1.308 +          ("is strictly less general than the declared type (see " ^ quote name ^ ")"))
   1.309 +      | Useless => err (Library.setmp show_sorts true (show_def (c, defT))
   1.310 +          "imposes additional sort constraints on the declared type of the constant"));
   1.311  
   1.312 +    val decl_defs = defs |> declare sg c |> fold (declare sg) (map #1 rhs_consts);
   1.313    in
   1.314 -      (case overloading sg c_decl ty of
   1.315 -         Useless =>
   1.316 -           err_in_defn sg name (Pretty.string_of (Pretty.chunks
   1.317 -           [Library.setmp show_sorts true def_txt (c_ty, ""), Pretty.str
   1.318 -              "imposes additional sort constraints on the declared type of the constant"]))   
   1.319 -       | ov =>
   1.320 -	 let 
   1.321 -	     val deps' = Defs.define deps c_ty name body
   1.322 -		 handle Defs.DEFS s => err_in_defn sg name ("DEFS: "^s) 
   1.323 -		      | Defs.CIRCULAR s => err_in_defn sg name (cycle_msg sg (false, s))
   1.324 -                      | Defs.INFINITE_CHAIN s => err_in_defn sg name (cycle_msg sg (true, s)) 
   1.325 -                      | Defs.CLASH (_, def1, def2) => err_in_defn sg name (
   1.326 -			  "clashing definitions "^ quote def1 ^" and "^ quote def2)
   1.327 -		      | Defs.FINAL cfinal =>
   1.328 -			err_in_defn sg name (Pretty.string_of (Pretty.block
   1.329 -			  ([Pretty.str "The constant",Pretty.brk 1] @
   1.330 -			   pretty_const cfinal @
   1.331 -			   [Pretty.brk 1,Pretty.str "has been declared final"]))) 
   1.332 -	 in
   1.333 -	     ((if ov = Plain andalso not overloaded then
   1.334 -		   warning (Pretty.string_of (Pretty.chunks
   1.335 -		     [def_txt (c_ty, ""), Pretty.str ("is strictly less general than the declared type (see " ^ quote name ^ ")")]))
   1.336 -	       else
   1.337 -		   ()); (deps', def::axms))
   1.338 -	 end)
   1.339 +    Defs.define decl_defs (c, defT) name rhs_consts
   1.340 +      handle Defs.DEFS msg => err ("DEFS: " ^ msg)   (* FIXME sys_error!? *)
   1.341 +        | Defs.CIRCULAR path => err (defs_circular pp path)
   1.342 +        | Defs.INFINITE_CHAIN path => err (defs_infinite_chain pp path)
   1.343 +        | Defs.CLASH (_, def1, def2) => err (defs_clash def1 def2)
   1.344 +        | Defs.FINAL const => err (defs_final pp const)
   1.345    end;
   1.346  
   1.347  
   1.348  (* add_defs *)
   1.349  
   1.350 -fun ext_defns prep_axm overloaded raw_axms thy =
   1.351 -  let
   1.352 -    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   1.353 -    val all_axioms = List.concat (map (Symtab.dest o #axioms o rep_theory) (thy :: ancestors));
   1.354 +local
   1.355  
   1.356 +fun gen_add_defs prep_axm overloaded raw_axms thy =
   1.357 +  let
   1.358 +    val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   1.359      val axms = map (prep_axm sign) raw_axms;
   1.360 -    val (const_deps', _) = Library.foldl (check_defn sign overloaded) ((const_deps, all_axioms), axms);
   1.361 +    val defs' = fold (check_def sign overloaded) axms defs;
   1.362    in
   1.363 -    make_theory sign const_deps' axioms oracles parents ancestors
   1.364 +    make_theory sign defs' axioms oracles parents ancestors
   1.365      |> add_axioms_i axms
   1.366    end;
   1.367  
   1.368 -val add_defs_i = ext_defns cert_axm;
   1.369 -val add_defs = ext_defns read_axm;
   1.370 +in
   1.371 +
   1.372 +val add_defs_i = gen_add_defs cert_axm;
   1.373 +val add_defs = gen_add_defs read_axm;
   1.374 +
   1.375 +end;
   1.376  
   1.377  
   1.378  (* add_finals *)
   1.379  
   1.380 -fun ext_finals prep_term overloaded raw_terms thy =
   1.381 +local
   1.382 +
   1.383 +fun gen_add_finals prep_term overloaded raw_terms thy =
   1.384    let
   1.385 -    val Theory {sign, const_deps, axioms, oracles, parents, ancestors} = thy;
   1.386 -    fun mk_final (tm, finals) =
   1.387 -	let
   1.388 -            fun err msg = raise TERM(msg,[tm])
   1.389 -            val (c,ty) = dest_Const tm
   1.390 -		handle TERM _ => err "Can only make constants final"
   1.391 -            val c_decl =
   1.392 -		(case Sign.const_type sign c of 
   1.393 -		     SOME T => T
   1.394 -		   | NONE => err ("Undeclared constant " ^ quote c))
   1.395 -	    val _ =
   1.396 -		case overloading sign c_decl ty of
   1.397 -		    NoOverloading => ()
   1.398 -		  | Useless => err "Sort constraints too strong"
   1.399 -		  | Plain => (if overloaded then () else warning "Type is more general than declared")
   1.400 -	    val finals = Defs.declare finals (c, c_decl) handle _ => finals
   1.401 -	in
   1.402 -	    Defs.finalize finals (c,ty)
   1.403 -	end
   1.404 -    val consts = map (prep_term sign) raw_terms;
   1.405 -    val const_deps' = foldl mk_final const_deps consts;
   1.406 -  in
   1.407 -    make_theory sign const_deps' axioms oracles parents ancestors
   1.408 -  end;
   1.409 +    val Theory {sign, defs, axioms, oracles, parents, ancestors} = thy;
   1.410 +    fun finalize tm finals =
   1.411 +      let
   1.412 +        fun err msg = raise TERM (msg, [tm]);    (* FIXME error!? *)
   1.413 +        val (c, defT) =
   1.414 +          (case tm of Const x => x
   1.415 +          | Free _ => err "Attempt to finalize variable (or undeclared constant)"
   1.416 +          | _ => err "Attempt to finalize non-constant term");
   1.417 +        val declT = Sign.the_const_type sign c
   1.418 +          handle TYPE (msg, _, _) => err msg;
   1.419 +        val _ =
   1.420 +          (case overloading sign overloaded declT defT of
   1.421 +            Clean => ()
   1.422 +          | Implcit => warning ("Finalizing " ^ quote c ^
   1.423 +              " at a strictly less general type than declared")
   1.424 +          | Useless => err "Sort constraints stronger than declared");
   1.425 +      in
   1.426 +        Defs.finalize (if_none (try (Defs.declare finals) (c, declT)) finals) (c, defT)
   1.427 +      end;
   1.428 +    val defs' = fold finalize (map (prep_term sign) raw_terms) defs;
   1.429 +  in make_theory sign defs' axioms oracles parents ancestors end;
   1.430  
   1.431 -local
   1.432 -  fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
   1.433 -  fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
   1.434 +fun read_term sg = Sign.simple_read_term sg TypeInfer.logicT;
   1.435 +fun cert_term sg = #1 o Sign.certify_term (Sign.pp sg) sg;
   1.436 +
   1.437  in
   1.438 -val add_finals = ext_finals read_term;
   1.439 -val add_finals_i = ext_finals cert_term;
   1.440 +
   1.441 +val add_finals = gen_add_finals read_term;
   1.442 +val add_finals_i = gen_add_finals cert_term;
   1.443 +
   1.444  end;
   1.445  
   1.446 -fun merge_final sg =
   1.447 -  let
   1.448 -    fun merge_single (tys,ty) =
   1.449 -      if exists (curry (Sign.typ_instance sg) ty) tys
   1.450 -      then tys
   1.451 -      else (ty::gen_rem (Sign.typ_instance sg) (tys,ty));
   1.452 -    fun merge ([],_) = []
   1.453 -      | merge (_,[]) = []
   1.454 -      | merge input = Library.foldl merge_single input;
   1.455 -  in
   1.456 -    SOME o merge
   1.457 -  end;
   1.458  
   1.459  
   1.460  (** additional theory data **)
   1.461 @@ -528,12 +526,12 @@
   1.462  (*merge list of theories from left to right, preparing extend*)
   1.463  fun prep_ext_merge thys =
   1.464    let
   1.465 -    val sign' = Sign.prep_ext_merge (map sign_of thys)
   1.466 +    val sign' = Sign.prep_ext_merge (map sign_of thys);
   1.467  
   1.468 -    val depss = map (#const_deps o rep_theory) thys;
   1.469 -    val deps' = foldl (uncurry Defs.merge) (hd depss) (tl depss)
   1.470 -      handle Defs.CIRCULAR namess => error (cycle_msg sign' (false, namess))
   1.471 -	   | Defs.INFINITE_CHAIN namess => error (cycle_msg sign' (true, namess))
   1.472 +    val defss = map (#defs o rep_theory) thys;
   1.473 +    val defs' = foldl (uncurry Defs.merge) (hd defss) (tl defss)
   1.474 +      handle Defs.CIRCULAR namess => error (defs_circular (Sign.pp sign') namess)
   1.475 +        | Defs.INFINITE_CHAIN namess => error (defs_infinite_chain (Sign.pp sign') namess);
   1.476  
   1.477      val axioms' = Symtab.empty;
   1.478  
   1.479 @@ -546,9 +544,7 @@
   1.480      val parents' = gen_distinct eq_thy thys;
   1.481      val ancestors' =
   1.482        gen_distinct eq_thy (parents' @ List.concat (map ancestors_of thys));
   1.483 -  in
   1.484 -    make_theory sign' deps' axioms' oracles' parents' ancestors'
   1.485 -  end;
   1.486 +  in make_theory sign' defs' axioms' oracles' parents' ancestors' end;
   1.487  
   1.488  
   1.489  end;