restored naming trick
authorblanchet
Mon Apr 28 00:54:31 2014 +0200 (2014-04-28)
changeset 567679b311dbd0f55
parent 56766 ba2fa4e99729
child 56768 06388a5cfb7c
restored naming trick
src/HOL/Tools/BNF/bnf_fp_def_sugar.ML
src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 28 00:54:30 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Apr 28 00:54:31 2014 +0200
     1.3 @@ -122,13 +122,12 @@
     1.4    val eq: T * T -> bool = op = o pairself (map #T);
     1.5  );
     1.6  
     1.7 -(* FIXME naming *)
     1.8  fun with_repaired_path f (fp_sugars as ({T = Type (s, _), ...} : fp_sugar) :: _) thy =
     1.9    thy
    1.10 -  (*|> Sign.root_path*)
    1.11 -  (*|> Sign.add_path (Long_Name.qualifier s)*)
    1.12 +  |> Sign.root_path
    1.13 +  |> Sign.add_path (Long_Name.qualifier s)
    1.14    |> f fp_sugars
    1.15 -  (*|> Sign.restore_naming thy*);
    1.16 +  |> Sign.restore_naming thy;
    1.17  
    1.18  fun fp_sugar_interpretation f = FP_Sugar_Interpretation.interpretation (with_repaired_path f);
    1.19  
     2.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 28 00:54:30 2014 +0200
     2.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Mon Apr 28 00:54:31 2014 +0200
     2.3 @@ -158,13 +158,12 @@
     2.4    val eq: T * T -> bool = op = o pairself #ctrs;
     2.5  );
     2.6  
     2.7 -(* FIXME naming *)
     2.8  fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
     2.9    thy
    2.10 -  (*|> Sign.root_path*)
    2.11 +  |> Sign.root_path
    2.12    |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
    2.13 -  (*|> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)*)
    2.14 -  (*|> Sign.restore_naming thy*);
    2.15 +  |> (fn thy => f (morph_ctr_sugar (Morphism.transfer_morphism thy) ctr_sugar) thy)
    2.16 +  |> Sign.restore_naming thy;
    2.17  
    2.18  fun ctr_sugar_interpretation f = Ctr_Sugar_Interpretation.interpretation (with_repaired_path f);
    2.19