# HG changeset patch # User wenzelm # Date 883317486 -3600 # Node ID 3e56603fde068243d7c34cd16386cccec2805227 # Parent 9b4c1db5aca170201dfd1f43b7863d9b9af7e0ea renamed Symtab.null to Symtab.empty; renamed Symtan.extend_new to Symtab.extend; diff -r 9b4c1db5aca1 -r 3e56603fde06 src/Pure/theory.ML --- a/src/Pure/theory.ML Sun Dec 28 14:56:44 1997 +0100 +++ b/src/Pure/theory.ML Sun Dec 28 14:58:06 1997 +0100 @@ -118,7 +118,7 @@ (* partial Pure theory *) -val pre_pure = make_thy Sign.pre_pure Symtab.null Symtab.null [] []; +val pre_pure = make_thy Sign.pre_pure Symtab.empty Symtab.empty [] []; @@ -143,10 +143,10 @@ val Theory {sign, axioms, oracles, parents, ancestors} = thy; val draft = Sign.is_draft sign; val axioms' = - Symtab.extend_new (if draft then axioms else Symtab.null, new_axms) + Symtab.extend (if draft then axioms else Symtab.empty, new_axms) handle Symtab.DUPS names => err_dup_axms names; val oracles' = - Symtab.extend_new (oracles, new_oras) + Symtab.extend (oracles, new_oras) handle Symtab.DUPS names => err_dup_oras names; val (parents', ancestors') = if draft then (parents, ancestors) else ([thy], thy :: ancestors); @@ -400,7 +400,7 @@ |> Sign.prep_ext |> Sign.add_path "/"; - val axioms' = Symtab.null; + val axioms' = Symtab.empty; fun eq_ora ((_, (_, s1: stamp)), (_, (_, s2))) = s1 = s2; val oracles' =