src/Pure/Isar/code.ML
changeset 67032 ed499d1252fc
parent 66332 489667636064
child 67147 dea94b1aabc3
     1.1 --- a/src/Pure/Isar/code.ML	Tue Nov 07 21:46:28 2017 +0100
     1.2 +++ b/src/Pure/Isar/code.ML	Wed Nov 08 15:31:14 2017 +0100
     1.3 @@ -805,7 +805,7 @@
     1.4    apfst (meta_rewrite thy)
     1.5    #> generic_assert_eqn strictness thy false
     1.6    #> Option.map (fn eqn => (const_eqn thy (fst eqn), eqn));
     1.7 -  
     1.8 +
     1.9  fun prep_eqns strictness thy =
    1.10    map_filter (prep_eqn strictness thy)
    1.11    #> AList.group (op =);
    1.12 @@ -1273,7 +1273,7 @@
    1.13          thy
    1.14          |> Sign.root_path
    1.15          |> Sign.add_path (Long_Name.qualifier tyco)
    1.16 -        |> f tyco 
    1.17 +        |> f tyco
    1.18          |> Sign.restore_naming thy));
    1.19  
    1.20  fun datatype_interpretation f =
    1.21 @@ -1459,7 +1459,7 @@
    1.22  val declare_abstract_eqn =
    1.23    code_declaration Morphism.thm generic_declare_abstract_eqn;
    1.24  
    1.25 -fun declare_aborting_global c = 
    1.26 +fun declare_aborting_global c =
    1.27    modify_specs (register_fun_spec c aborting);
    1.28  
    1.29  fun declare_unimplemented_global c =