src/HOL/Tools/ATP/atp_translate.ML
changeset 44494 a77901b3774e
parent 44493 c2602c5d4b0a
child 44495 4c2242c8a96c
     1.1 --- a/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
     1.2 +++ b/src/HOL/Tools/ATP/atp_translate.ML	Thu Aug 25 14:25:07 2011 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4      Chained
     1.5  
     1.6    datatype order = First_Order | Higher_Order
     1.7 -  datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
     1.8 +  datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
     1.9    datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    1.10    datatype type_level =
    1.11      All_Types |
    1.12 @@ -522,7 +522,7 @@
    1.13    Chained
    1.14  
    1.15  datatype order = First_Order | Higher_Order
    1.16 -datatype polymorphism = Polymorphic | Monomorphic | Mangled_Monomorphic
    1.17 +datatype polymorphism = Polymorphic | Raw_Monomorphic | Mangled_Monomorphic
    1.18  datatype soundness = Unsound | Sound_Modulo_Infiniteness | Sound
    1.19  datatype type_level =
    1.20    All_Types |
    1.21 @@ -544,10 +544,10 @@
    1.22    (case try (unprefix "poly_") s of
    1.23       SOME s => (SOME Polymorphic, s)
    1.24     | NONE =>
    1.25 -     case try (unprefix "mono_") s of
    1.26 -       SOME s => (SOME Monomorphic, s)
    1.27 +     case try (unprefix "raw_mono_") s of
    1.28 +       SOME s => (SOME Raw_Monomorphic, s)
    1.29       | NONE =>
    1.30 -       case try (unprefix "mangled_") s of
    1.31 +       case try (unprefix "mono_") s of
    1.32           SOME s => (SOME Mangled_Monomorphic, s)
    1.33         | NONE => (NONE, s))
    1.34    ||> (fn s =>