more explicit name
authorhaftmann
Thu Dec 27 21:01:08 2012 +0100 (2012-12-27)
changeset 50625e3d25e751d05
parent 50624 4d0997abce79
child 50626 e21485358c56
more explicit name
src/Tools/Code/code_ml.ML
src/Tools/Code/code_thingol.ML
     1.1 --- a/src/Tools/Code/code_ml.ML	Thu Dec 27 16:49:12 2012 +0100
     1.2 +++ b/src/Tools/Code/code_ml.ML	Thu Dec 27 21:01:08 2012 +0100
     1.3 @@ -51,7 +51,7 @@
     1.4  
     1.5  (** SML serializer **)
     1.6  
     1.7 -fun print_sml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
     1.8 +fun print_sml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
     1.9    let
    1.10      fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    1.11        | print_tyco_expr (tyco, [ty]) =
    1.12 @@ -110,7 +110,7 @@
    1.13                  else print_app is_pseudo_fun some_thm vars fxy app
    1.14              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
    1.15      and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
    1.16 -      if is_cons c then
    1.17 +      if is_constr c then
    1.18          let val k = length dom in
    1.19            if k < 2 orelse length ts = k
    1.20            then (str o deresolve) c
    1.21 @@ -355,7 +355,7 @@
    1.22  
    1.23  (** OCaml serializer **)
    1.24  
    1.25 -fun print_ocaml_stmt tyco_syntax const_syntax reserved is_cons deresolve =
    1.26 +fun print_ocaml_stmt tyco_syntax const_syntax reserved is_constr deresolve =
    1.27    let
    1.28      fun print_tyco_expr (tyco, []) = (str o deresolve) tyco
    1.29        | print_tyco_expr (tyco, [ty]) =
    1.30 @@ -410,7 +410,7 @@
    1.31                  else print_app is_pseudo_fun some_thm vars fxy app
    1.32              | NONE => print_case is_pseudo_fun some_thm vars fxy case_expr)
    1.33      and print_app_expr is_pseudo_fun some_thm vars (app as ({ name = c, dicts = dss, dom = dom, ... }, ts)) =
    1.34 -      if is_cons c then
    1.35 +      if is_constr c then
    1.36          let val k = length dom in
    1.37            if length ts = k
    1.38            then (str o deresolve) c
    1.39 @@ -794,7 +794,7 @@
    1.40      (* print statements *)
    1.41      fun print_stmt prefix_fragments (_, stmt) = print_ml_stmt
    1.42        tyco_syntax const_syntax (make_vars reserved_syms)
    1.43 -      (Code_Thingol.is_cons program) (deresolver prefix_fragments) stmt
    1.44 +      (Code_Thingol.is_constr program) (deresolver prefix_fragments) stmt
    1.45        |> apfst SOME;
    1.46  
    1.47      (* print modules *)
     2.1 --- a/src/Tools/Code/code_thingol.ML	Thu Dec 27 16:49:12 2012 +0100
     2.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Dec 27 21:01:08 2012 +0100
     2.3 @@ -84,7 +84,7 @@
     2.4    val empty_funs: program -> string list
     2.5    val map_terms_bottom_up: (iterm -> iterm) -> iterm -> iterm
     2.6    val map_terms_stmt: (iterm -> iterm) -> stmt -> stmt
     2.7 -  val is_cons: program -> string -> bool
     2.8 +  val is_constr: program -> string -> bool
     2.9    val is_case: stmt -> bool
    2.10    val labelled_name: theory -> program -> string -> string
    2.11    val group_stmts: theory -> program
    2.12 @@ -464,7 +464,7 @@
    2.13            inst_params = map_classparam_instances_as_term f inst_params,
    2.14            superinst_params = map_classparam_instances_as_term f superinst_params };
    2.15  
    2.16 -fun is_cons program name = case Graph.get_node program name
    2.17 +fun is_constr program name = case Graph.get_node program name
    2.18   of Datatypecons _ => true
    2.19    | _ => false;
    2.20