# 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