src/Pure/Isar/code.ML
changeset 66133 0b635a6774fb
parent 66132 5844a096c462
child 66149 4bf16fb7c14d
     1.1 --- a/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.2 +++ b/src/Pure/Isar/code.ML	Tue Jun 20 08:01:56 2017 +0200
     1.3 @@ -1020,9 +1020,7 @@
     1.4      fun pretty_equations const thms =
     1.5        (Pretty.block o Pretty.fbreaks)
     1.6          (Pretty.str (string_of_const thy const) :: map (Thm.pretty_thm_item ctxt) thms);
     1.7 -    fun pretty_function (const, Unimplemented) =
     1.8 -          pretty_equations const []
     1.9 -      | pretty_function (const, Eqns_Default (_, eqns_lazy)) =
    1.10 +    fun pretty_function (const, Eqns_Default (_, eqns_lazy)) =
    1.11            pretty_equations const (map fst (Lazy.force eqns_lazy))
    1.12        | pretty_function (const, Eqns eqns) =
    1.13            pretty_equations const (map fst eqns)
    1.14 @@ -1053,6 +1051,7 @@
    1.15      val functions = functions_of spec
    1.16        |> Symtab.dest
    1.17        |> (map o apsnd) (snd o fst)
    1.18 +      |> filter (fn (_, Unimplemented) => false | _ => true)
    1.19        |> sort (string_ord o apply2 fst);
    1.20      val datatypes = types_of spec
    1.21        |> Symtab.dest