src/Pure/Isar/expression.ML
changeset 29006 abe0f11cfa4e
parent 28994 49f602ae24e5
child 29020 3e95d28114a1
     1.1 --- a/src/Pure/Isar/expression.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/Isar/expression.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -134,8 +134,8 @@
     1.4          if null dups then () else error (message ^ commas dups)
     1.5        end;
     1.6  
     1.7 -    fun match_bind (n, b) = (n = Name.name_of b);
     1.8 -    fun bind_eq (b1, b2) = (Name.name_of b1 = Name.name_of b2);
     1.9 +    fun match_bind (n, b) = (n = Binding.base_name b);
    1.10 +    fun bind_eq (b1, b2) = (Binding.base_name b1 = Binding.base_name b2);
    1.11        (* FIXME: cannot compare bindings for equality. *)
    1.12  
    1.13      fun params_loc loc =
    1.14 @@ -177,8 +177,8 @@
    1.15  
    1.16      val (implicit, expr') = params_expr expr;
    1.17  
    1.18 -    val implicit' = map (#1 #> Name.name_of) implicit;
    1.19 -    val fixed' = map (#1 #> Name.name_of) fixed;
    1.20 +    val implicit' = map (#1 #> Binding.base_name) implicit;
    1.21 +    val fixed' = map (#1 #> Binding.base_name) fixed;
    1.22      val _ = reject_dups "Duplicate fixed parameter(s): " fixed';
    1.23      val implicit'' = if strict then []
    1.24        else let val _ = reject_dups
    1.25 @@ -385,7 +385,7 @@
    1.26        end;
    1.27  
    1.28  fun finish_primitive parms _ (Fixes fixes) = Fixes (map (fn (binding, _, mx) =>
    1.29 -      let val x = Name.name_of binding
    1.30 +      let val x = Binding.base_name binding
    1.31        in (binding, AList.lookup (op =) parms x, mx) end) fixes)
    1.32    | finish_primitive _ _ (Constrains _) = Constrains []
    1.33    | finish_primitive _ close (Assumes asms) = close (Assumes asms)
    1.34 @@ -396,7 +396,7 @@
    1.35    let
    1.36      val thy = ProofContext.theory_of ctxt;
    1.37      val (parm_names, parm_types) = NewLocale.params_of thy loc |>
    1.38 -      map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
    1.39 +      map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
    1.40      val (asm, defs) = NewLocale.specification_of thy loc;
    1.41      val (morph, _) = inst_morph (parm_names, parm_types) (prfx, inst) ctxt;
    1.42      val asm' = Option.map (Morphism.term morph) asm;
    1.43 @@ -440,7 +440,7 @@
    1.44      fun prep_inst (loc, (prfx, inst)) (i, insts, ctxt) =
    1.45        let
    1.46          val (parm_names, parm_types) = NewLocale.params_of thy loc |>
    1.47 -          map (fn (b, SOME T, _) => (Name.name_of b, T)) |> split_list;
    1.48 +          map (fn (b, SOME T, _) => (Binding.base_name b, T)) |> split_list;
    1.49          val inst' = parse_inst parm_names inst ctxt;
    1.50          val parm_types' = map (TypeInfer.paramify_vars o
    1.51            Term.map_type_tvar (fn ((x, _), S) => TVar ((x, i), S)) o Logic.varifyT) parm_types;
    1.52 @@ -473,7 +473,7 @@
    1.53      val (insts, elems, concl, ctxt) = prep_concl raw_concl (insts', elems'', ctxt'');
    1.54  
    1.55      (* Retrieve parameter types *)
    1.56 -    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Name.name_of o #1) fixes) |
    1.57 +    val xs = fold (fn Fixes fixes => (fn ps => ps @ map (Binding.base_name o #1) fixes) |
    1.58        _ => fn ps => ps) (Fixes fors :: elems) [];
    1.59      val (Ts, ctxt') = fold_map ProofContext.inferred_param xs ctxt; 
    1.60      val parms = xs ~~ Ts;  (* params from expression and elements *)