1.1 --- a/src/Pure/Isar/constdefs.ML	Fri May 07 20:33:14 2004 +0200
     1.2 +++ b/src/Pure/Isar/constdefs.ML	Fri May 07 20:33:37 2004 +0200
     1.3 @@ -42,9 +42,12 @@
     1.4      val ctxt =
     1.5        ProofContext.init thy |> ProofContext.add_fixes
     1.6          (flat (map (fn (As, T) => map (fn A => (A, T, None)) As) structs));
     1.7 -    val (ctxt', mx) =
     1.8 -      (case decl of None => (ctxt, Syntax.NoSyn) | Some (x, raw_T, mx) =>
     1.9 -        (ProofContext.add_fixes [(x, apsome (prep_typ ctxt) raw_T, Some mx)] ctxt, mx));
    1.10 +    val (ctxt', d, mx) =
    1.11 +      (case decl of None => (ctxt, None, Syntax.NoSyn) | Some (x, raw_T, mx) =>
    1.12 +        let
    1.13 +          val x' = Syntax.const_name x mx and mx' = Syntax.fix_mixfix x mx;
    1.14 +          val T = apsome (prep_typ ctxt) raw_T;
    1.15 +        in (ProofContext.add_fixes_liberal [(x', T, Some mx')] ctxt, Some x', mx') end);
    1.16  
    1.17      val prop = prep_term ctxt' raw_prop;
    1.18      val concl = Logic.strip_imp_concl prop;
    1.19 @@ -53,9 +56,9 @@
    1.20      val head = Term.head_of lhs;
    1.21      val (c, T) = Term.dest_Free head handle TERM _ =>
    1.22        err "Locally fixed variable required as head of definition:" [head];
    1.23 -    val _ = (case decl of None => () | Some (d, _, _) =>
    1.24 -      if c <> d then
    1.25 -        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote d) []
    1.26 +    val _ = (case d of None => () | Some c' =>
    1.27 +      if c <> c' then
    1.28 +        err ("Head of definition " ^ quote c ^ " differs from declaration " ^ quote c') []
    1.29        else ());
    1.30  
    1.31      val def = Term.subst_atomic [(Free (c, T), Const (Sign.full_name sign c, T))] prop;
    1.32 @@ -75,9 +78,9 @@
    1.33        |> foldl_map (gen_constdef prep_typ prep_term prep_att structs);
    1.34    in Pretty.writeln (pretty_constdefs (Theory.sign_of thy') decls); thy' end;
    1.35  
    1.36 -val add_constdefs = gen_constdefs ProofContext.read_vars
    1.37 -  ProofContext.read_typ ProofContext.read_term Attrib.global_attribute;
    1.38 -val add_constdefs_i = gen_constdefs ProofContext.cert_vars
    1.39 +val add_constdefs = gen_constdefs ProofContext.read_vars_liberal
    1.40 +  ProofContext.read_typ ProofContext.read_term_liberal Attrib.global_attribute;
    1.41 +val add_constdefs_i = gen_constdefs ProofContext.cert_vars_liberal
    1.42    ProofContext.cert_typ ProofContext.cert_term (K I);
    1.43  
    1.44  end;