# HG changeset patch # User wenzelm # Date 1684156459 -7200 # Node ID bb60ea7318d63d55675c86e0054a89a66425d190 # Parent 64f81d011a90d0338ec8e8bf3c5acca9c8ce0c06 tuned whitespace; diff -r 64f81d011a90 -r bb60ea7318d6 src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Mon May 15 15:04:37 2023 +0200 +++ b/src/Pure/Isar/code.ML Mon May 15 15:14:19 2023 +0200 @@ -1373,9 +1373,7 @@ | NONE => thy; val declare_abstype_global = generic_declare_abstype Strict; - -val declare_abstype = - code_declaration Morphism.thm generic_declare_abstype; +val declare_abstype = code_declaration Morphism.thm generic_declare_abstype; (* functions *) @@ -1448,14 +1446,10 @@ end; val declare_default_eqns_global = generic_declare_eqns true Silent; - -val declare_default_eqns = - silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true); +val declare_default_eqns = silent_code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns true); val declare_eqns_global = generic_declare_eqns false Strict; - -val declare_eqns = - code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false); +val declare_eqns = code_declaration (map o apfst o Morphism.thm) (generic_declare_eqns false); val add_eqn_global = generic_add_eqn Strict; @@ -1466,9 +1460,7 @@ | NONE => thy; val declare_abstract_eqn_global = generic_declare_abstract_eqn Strict; - -val declare_abstract_eqn = - code_declaration Morphism.thm generic_declare_abstract_eqn; +val declare_abstract_eqn = code_declaration Morphism.thm generic_declare_abstract_eqn; fun declare_aborting_global c = modify_specs (register_fun_spec c aborting);