src/Pure/Isar/object_logic.ML
changeset 14226 7afe0e5bcc83
parent 13376 59975b8417e2
child 14743 81001d6cb8c0
     1.1 --- a/src/Pure/Isar/object_logic.ML	Fri Oct 10 11:13:29 2003 +0200
     1.2 +++ b/src/Pure/Isar/object_logic.ML	Fri Oct 10 12:12:35 2003 +0200
     1.3 @@ -69,10 +69,24 @@
     1.4  fun new_judgment name (None, rules) = (Some name, rules)
     1.5    | new_judgment _ (Some _, _) = error "Attempt to redeclare object-logic judgment";
     1.6  
     1.7 +fun add_final name thy =
     1.8 +  let
     1.9 +    val typ = case Sign.const_type (sign_of thy) name of
    1.10 +		Some T => T
    1.11 +	      | None => error "Internal error in ObjectLogic.gen_add_judgment";
    1.12 +  in
    1.13 +    Theory.add_finals_i false [Const(name,typ)] thy
    1.14 +  end;
    1.15 +
    1.16  fun gen_add_judgment add_consts (name, T, syn) thy =
    1.17 -  thy
    1.18 -  |> add_consts [(name, T, syn)]
    1.19 -  |> ObjectLogicData.map (new_judgment (Sign.full_name (Theory.sign_of thy) name));
    1.20 +  let
    1.21 +    val fullname = Sign.full_name (Theory.sign_of thy) name;
    1.22 +  in
    1.23 +    thy
    1.24 +    |> add_consts [(name, T, syn)]
    1.25 +    |> add_final fullname
    1.26 +    |> ObjectLogicData.map (new_judgment fullname)
    1.27 +  end;
    1.28  
    1.29  in
    1.30