# HG changeset patch # User skalberg # Date 1065780755 -7200 # Node ID 7afe0e5bcc8333ccc714c37074a0068d73dfe2da # Parent 6d1026266e2bf9bf364beaeca87f2c7bf3825bb4 Made judgments automatically declared final. diff -r 6d1026266e2b -r 7afe0e5bcc83 src/Pure/Isar/object_logic.ML --- a/src/Pure/Isar/object_logic.ML Fri Oct 10 11:13:29 2003 +0200 +++ b/src/Pure/Isar/object_logic.ML Fri Oct 10 12:12:35 2003 +0200 @@ -69,10 +69,24 @@ fun new_judgment name (None, rules) = (Some name, rules) | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment"; +fun add_final name thy = + let + val typ = case Sign.const_type (sign_of thy) name of + Some T => T + | None => error "Internal error in ObjectLogic.gen_add_judgment"; + in + Theory.add_finals_i false [Const(name,typ)] thy + end; + fun gen_add_judgment add_consts (name, T, syn) thy = - thy - |> add_consts [(name, T, syn)] - |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name)); + let + val fullname = Sign.full_name (Theory.sign_of thy) name; + in + thy + |> add_consts [(name, T, syn)] + |> add_final fullname + |> ObjectLogicData.map (new_judgment fullname) + end; in