src/Tools/isac/BaseDefinitions/rule-set.sml
changeset 59879 33449c96d99f
parent 59878 3163e63a5111
child 59885 59c5dd27d589
     1.1 --- a/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Apr 15 11:37:43 2020 +0200
     1.2 +++ b/src/Tools/isac/BaseDefinitions/rule-set.sml	Wed Apr 15 13:47:56 2020 +0200
     1.3 @@ -115,7 +115,7 @@
     1.4  (* datastructure for KEStore_Elems, intermediate for thehier *)
     1.5  type for_kestore = 
     1.6    (id *     (* id unique within Isac *)
     1.7 -  (ThyC.theory' *  (* just for assignment in thehier, not appropriate for parsing etc *)
     1.8 +  (ThyC.id *  (* just for assignment in thehier, not appropriate for parsing etc *)
     1.9      T))     (* ((#id o rep) T) = id   by coding discipline *)
    1.10  fun equal ((id1, (_, _)), (id2, (_, _))) = id1 = id2
    1.11