src/Pure/Isar/proof_context.ML
changeset 29006 abe0f11cfa4e
parent 28965 1de908189869
child 29318 6337d1cb2ba0
     1.1 --- a/src/Pure/Isar/proof_context.ML	Fri Dec 05 18:42:39 2008 +0100
     1.2 +++ b/src/Pure/Isar/proof_context.ML	Fri Dec 05 18:43:42 2008 +0100
     1.3 @@ -1012,7 +1012,7 @@
     1.4  fun prep_vars prep_typ internal =
     1.5    fold_map (fn (raw_b, raw_T, raw_mx) => fn ctxt =>
     1.6      let
     1.7 -      val raw_x = Name.name_of raw_b;
     1.8 +      val raw_x = Binding.base_name raw_b;
     1.9        val (x, mx) = Syntax.const_mixfix raw_x raw_mx;
    1.10        val _ = Syntax.is_identifier (no_skolem internal x) orelse
    1.11          error ("Illegal variable name: " ^ quote x);
    1.12 @@ -1122,7 +1122,7 @@
    1.13  fun gen_fixes prep raw_vars ctxt =
    1.14    let
    1.15      val (vars, _) = prep raw_vars ctxt;
    1.16 -    val (xs', ctxt') = Variable.add_fixes (map (Name.name_of o #1) vars) ctxt;
    1.17 +    val (xs', ctxt') = Variable.add_fixes (map (Binding.base_name o #1) vars) ctxt;
    1.18      val ctxt'' =
    1.19        ctxt'
    1.20        |> fold_map declare_var (map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars)