src/Pure/Isar/context_rules.ML
changeset 15973 5fd94d84470f
parent 15801 d2f5ca3c048d
child 16424 18a07ad8fea8
     1.1 --- a/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:43 2005 +0200
     1.2 +++ b/src/Pure/Isar/context_rules.ML	Tue May 17 10:19:44 2005 +0200
     1.3 @@ -111,7 +111,7 @@
     1.4  fun print_rules prt x (Rules {rules, ...}) =
     1.5    let
     1.6      fun prt_kind (i, b) =
     1.7 -      Pretty.big_list (valOf (assoc (kind_names, (i, b))) ^ ":")
     1.8 +      Pretty.big_list (the (assoc (kind_names, (i, b))) ^ ":")
     1.9          (List.mapPartial (fn (_, (k, th)) => if k = (i, b) then SOME (prt x th) else NONE)
    1.10            (sort (Int.compare o pairself fst) rules));
    1.11    in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;