src/Pure/theory.ML
changeset 19693 ab816ca8df06
parent 19630 d370c3f5d3b2
child 19700 e02af528ceef
equal deleted inserted replaced
19692:bad13b32c0f3 19693:ab816ca8df06
   118     let
   118     let
   119       val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
   119       val Thy {axioms = _, defs = defs1, oracles = oracles1} = thy1;
   120       val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
   120       val Thy {axioms = _, defs = defs2, oracles = oracles2} = thy2;
   121 
   121 
   122       val axioms = NameSpace.empty_table;
   122       val axioms = NameSpace.empty_table;
   123       val defs = Defs.merge (defs1, defs2);
   123       val defs = Defs.merge pp (defs1, defs2);
   124       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   124       val oracles = NameSpace.merge_tables (eq_snd (op =)) (oracles1, oracles2)
   125         handle Symtab.DUPS dups => err_dup_oras dups;
   125         handle Symtab.DUPS dups => err_dup_oras dups;
   126     in make_thy (axioms, defs, oracles) end;
   126     in make_thy (axioms, defs, oracles) end;
   127 
   127 
   128   fun print _ _ = ();
   128   fun print _ _ = ();
   254 
   254 
   255 (* check_def *)
   255 (* check_def *)
   256 
   256 
   257 fun check_def thy unchecked overloaded (bname, tm) defs =
   257 fun check_def thy unchecked overloaded (bname, tm) defs =
   258   let
   258   let
   259     val pp = Sign.pp thy;
       
   260     fun prt_const (c, T) =
       
   261      [Pretty.str c, Pretty.str " ::", Pretty.brk 1,
       
   262       Pretty.quote (Pretty.typ pp (Type.freeze_type T))];
       
   263 
       
   264     val name = Sign.full_name thy bname;
   259     val name = Sign.full_name thy bname;
   265     val (lhs_const, rhs) = Sign.cert_def pp tm;
   260     val (lhs_const, rhs) = Sign.cert_def (Sign.pp thy) tm;
   266     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   261     val rhs_consts = fold_aterms (fn Const const => insert (op =) const | _ => I) rhs [];
   267     val _ = check_overloading thy overloaded lhs_const;
   262     val _ = check_overloading thy overloaded lhs_const;
   268   in
   263   in
   269     defs |> Defs.define (Sign.const_typargs thy) unchecked true (Context.theory_name thy)
   264     defs |> Defs.define (Sign.pp thy) (Sign.consts_of thy) unchecked true (Context.theory_name thy)
   270       name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   265       name (prep_const thy lhs_const) (map (prep_const thy) rhs_consts)
   271   end
   266   end
   272   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   267   handle ERROR msg => cat_error msg (Pretty.string_of (Pretty.block
   273    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   268    [Pretty.str ("The error(s) above occurred in definition " ^ quote bname ^ ":"),
   274     Pretty.fbrk, Pretty.quote (Pretty.term (Sign.pp thy) tm)]));
   269     Pretty.fbrk, Pretty.quote (Sign.pretty_term thy tm)]));
   275 
   270 
   276 
   271 
   277 (* add_defs(_i) *)
   272 (* add_defs(_i) *)
   278 
   273 
   279 local
   274 local
   300 fun gen_add_finals prep_term overloaded args thy =
   295 fun gen_add_finals prep_term overloaded args thy =
   301   let
   296   let
   302     fun const_of (Const const) = const
   297     fun const_of (Const const) = const
   303       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
   298       | const_of (Free _) = error "Attempt to finalize variable (or undeclared constant)"
   304       | const_of _ = error "Attempt to finalize non-constant term";
   299       | const_of _ = error "Attempt to finalize non-constant term";
   305     fun specify (c, T) = Defs.define (Sign.const_typargs thy) false false (Context.theory_name thy)
   300     fun specify (c, T) = Defs.define (Sign.pp thy) (Sign.consts_of thy) false false
   306       (c ^ " axiom") (prep_const thy (c, T)) [];
   301       (Context.theory_name thy) (c ^ " axiom") (prep_const thy (c, T)) [];
   307     val finalize = specify o check_overloading thy overloaded o
   302     val finalize = specify o check_overloading thy overloaded o
   308       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   303       const_of o Sign.no_vars (Sign.pp thy) o prep_term thy;
   309   in thy |> map_defs (fold finalize args) end;
   304   in thy |> map_defs (fold finalize args) end;
   310 
   305 
   311 in
   306 in