tuned;
authorwenzelm
Sun May 26 21:05:03 2013 +0200 (2013-05-26)
changeset 5216151eca565b153
parent 52160 7746c9f1baf3
child 52162 896ebb4646d8
tuned;
src/Pure/pure_thy.ML
src/Pure/term.ML
src/Tools/Code/code_target.ML
src/Tools/Code/code_thingol.ML
     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
     2.1 --- a/src/Pure/term.ML	Sun May 26 20:42:43 2013 +0200
     2.2 +++ b/src/Pure/term.ML	Sun May 26 21:05:03 2013 +0200
     2.3 @@ -159,7 +159,6 @@
     2.4    val maxidx_term: term -> int -> int
     2.5    val has_abs: term -> bool
     2.6    val dest_abs: string * typ * term -> string * term
     2.7 -  val dummy_patternN: string
     2.8    val dummy_pattern: typ -> term
     2.9    val dummy: term
    2.10    val dummy_prop: term
    2.11 @@ -925,9 +924,7 @@
    2.12  
    2.13  (* dummy patterns *)
    2.14  
    2.15 -val dummy_patternN = "dummy_pattern";
    2.16 -
    2.17 -fun dummy_pattern T = Const (dummy_patternN, T);
    2.18 +fun dummy_pattern T = Const ("dummy_pattern", T);
    2.19  val dummy = dummy_pattern dummyT;
    2.20  val dummy_prop = dummy_pattern propT;
    2.21  
     3.1 --- a/src/Tools/Code/code_target.ML	Sun May 26 20:42:43 2013 +0200
     3.2 +++ b/src/Tools/Code/code_target.ML	Sun May 26 21:05:03 2013 +0200
     3.3 @@ -419,7 +419,7 @@
     3.4      val value_name = "Value.value.value"
     3.5      val program = prepared_program
     3.6        |> Graph.new_node (value_name,
     3.7 -          Code_Thingol.Fun (Term.dummy_patternN, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
     3.8 +          Code_Thingol.Fun (@{const_name dummy_pattern}, (((vs', ty'), [(([IVar NONE], t), (NONE, true))]), NONE)))
     3.9        |> fold (curry (perhaps o try o Graph.add_edge) value_name) consts;
    3.10      val (program_code, deresolve) = produce (mounted_serializer program);
    3.11      val value_name' = the (deresolve value_name);
     4.1 --- a/src/Tools/Code/code_thingol.ML	Sun May 26 20:42:43 2013 +0200
     4.2 +++ b/src/Tools/Code/code_thingol.ML	Sun May 26 21:05:03 2013 +0200
     4.3 @@ -938,24 +938,24 @@
     4.4      val ty = fastype_of t;
     4.5      val vs = fold_term_types (K (fold_atyps (insert (eq_fst op =)
     4.6        o dest_TFree))) t [];
     4.7 -    val t' = annotate thy algbr eqngr (Term.dummy_patternN, ty) [] t;
     4.8 +    val t' = annotate thy algbr eqngr (@{const_name dummy_pattern}, ty) [] t;
     4.9      val stmt_value =
    4.10        fold_map (translate_tyvar_sort thy algbr eqngr false) vs
    4.11        ##>> translate_typ thy algbr eqngr false ty
    4.12        ##>> translate_term thy algbr eqngr false NONE (t', NONE)
    4.13        #>> (fn ((vs, ty), t) => Fun
    4.14 -        (Term.dummy_patternN, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
    4.15 +        (@{const_name dummy_pattern}, (((vs, ty), [(([], t), (NONE, true))]), NONE)));
    4.16      fun term_value (dep, (naming, program1)) =
    4.17        let
    4.18          val Fun (_, ((vs_ty, [(([], t), _)]), _)) =
    4.19 -          Graph.get_node program1 Term.dummy_patternN;
    4.20 -        val deps = Graph.immediate_succs program1 Term.dummy_patternN;
    4.21 -        val program2 = Graph.del_node Term.dummy_patternN program1;
    4.22 +          Graph.get_node program1 @{const_name dummy_pattern};
    4.23 +        val deps = Graph.immediate_succs program1 @{const_name dummy_pattern};
    4.24 +        val program2 = Graph.del_node @{const_name dummy_pattern} program1;
    4.25          val deps_all = Graph.all_succs program2 deps;
    4.26          val program3 = Graph.restrict (member (op =) deps_all) program2;
    4.27        in (((naming, program3), ((vs_ty, t), deps)), (dep, (naming, program2))) end;
    4.28    in
    4.29 -    ensure_stmt ((K o K) NONE) pair stmt_value Term.dummy_patternN
    4.30 +    ensure_stmt ((K o K) NONE) pair stmt_value @{const_name dummy_pattern}
    4.31      #> snd
    4.32      #> term_value
    4.33    end;