--- a/src/Pure/Isar/code.ML Wed Nov 08 17:34:32 2017 +0100
+++ b/src/Pure/Isar/code.ML Wed Nov 08 17:36:21 2017 +0100
@@ -805,7 +805,7 @@
apfst (meta_rewrite thy)
#> generic_assert_eqn strictness thy false
#> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn));
-
+
fun prep_eqns strictness thy =
map_filter (prep_eqn strictness thy)
#> AList.group (op =);
@@ -1273,7 +1273,7 @@
thy
|> Sign.root_path
|> Sign.add_path (Long_Name.qualifier tyco)
- |> f tyco
+ |> f tyco
|> Sign.restore_naming thy));
fun datatype_interpretation f =
@@ -1459,7 +1459,7 @@
val declare_abstract_eqn =
code_declaration Morphism.thm generic_declare_abstract_eqn;
-fun declare_aborting_global c =
+fun declare_aborting_global c =
modify_specs (register_fun_spec c aborting);
fun declare_unimplemented_global c =