src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML
changeset 56376 5a93b8f928a2
parent 56345 228e30cb111d
child 56522 f54003750e7d
     1.1 --- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:22 2014 +0200
     1.2 +++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML	Thu Apr 03 10:51:24 2014 +0200
     1.3 @@ -158,7 +158,14 @@
     1.4    val eq: T * T -> bool = op = o pairself #ctrs;
     1.5  );
     1.6  
     1.7 -val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation;
     1.8 +fun with_repaired_path f (ctr_sugar as {ctrs = ctr1 :: _, ...} : ctr_sugar) thy =
     1.9 +  thy
    1.10 +  |> Sign.root_path
    1.11 +  |> Sign.add_path (Long_Name.qualifier (fst (dest_Type (body_type (fastype_of ctr1)))))
    1.12 +  |> f ctr_sugar
    1.13 +  |> Sign.restore_naming thy;
    1.14 +
    1.15 +val ctr_sugar_interpretation = Ctr_Sugar_Interpretation.interpretation o with_repaired_path;
    1.16  
    1.17  fun register_ctr_sugar key ctr_sugar =
    1.18    Local_Theory.declaration {syntax = false, pervasive = true}