src/Pure/pure_thy.ML
changeset 52161 51eca565b153
parent 52160 7746c9f1baf3
child 52211 66bc827e37f8
     1.1 --- a/src/Pure/pure_thy.ML	Sun May 26 20:42:43 2013 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Sun May 26 21:05:03 2013 +0200
     1.3 @@ -164,7 +164,7 @@
     1.4      ("_context_xconst", typ "longid_position => logic", Delimfix "XCONST _"),
     1.5      ("_context_xconst", typ "longid_position => aprop", Delimfix "XCONST _"),
     1.6      (const "==>",   typ "prop => prop => prop",        Delimfix "op ==>"),
     1.7 -    (const Term.dummy_patternN, typ "aprop",           Delimfix "'_"),
     1.8 +    (const "dummy_pattern", typ "aprop",               Delimfix "'_"),
     1.9      ("_sort_constraint", typ "type => prop",           Delimfix "(1SORT'_CONSTRAINT/(1'(_')))"),
    1.10      (const "Pure.term", typ "logic => prop",           Delimfix "TERM _"),
    1.11      (const "Pure.conjunction", typ "prop => prop => prop", Infixr ("&&&", 2))]
    1.12 @@ -194,12 +194,12 @@
    1.13      (Binding.name "all", typ "('a => prop) => prop", Binder ("!!", 0, 0)),
    1.14      (Binding.name "prop", typ "prop => prop", NoSyn),
    1.15      (Binding.name "TYPE", typ "'a itself", NoSyn),
    1.16 -    (Binding.name Term.dummy_patternN, typ "'a", Delimfix "'_")]
    1.17 +    (Binding.name "dummy_pattern", typ "'a", Delimfix "'_")]
    1.18    #> Theory.add_deps_global "==" ("==", typ "'a => 'a => prop") []
    1.19    #> Theory.add_deps_global "==>" ("==>", typ "prop => prop => prop") []
    1.20    #> Theory.add_deps_global "all" ("all", typ "('a => prop) => prop") []
    1.21    #> Theory.add_deps_global "TYPE" ("TYPE", typ "'a itself") []
    1.22 -  #> Theory.add_deps_global Term.dummy_patternN (Term.dummy_patternN, typ "'a") []
    1.23 +  #> Theory.add_deps_global "dummy_pattern" ("dummy_pattern", typ "'a") []
    1.24    #> Sign.parse_ast_translation Syntax_Trans.pure_parse_ast_translation
    1.25    #> Sign.parse_translation Syntax_Trans.pure_parse_translation
    1.26    #> Sign.print_ast_translation Syntax_Trans.pure_print_ast_translation